Let X and Tx be given.
Assume Hlc: locally_compact X Tx.
Assume HH: Hausdorff_space X Tx.
We will prove ∃Y Ty : set, one_point_compactification X Tx Y Ty.
Set p to be the term X.
Set Y to be the term X ∪ {p}.
Set Ty to be the term {U ∈ 𝒫 Y|(p ∉ U ∧ U ∈ Tx) ∨ (p ∈ U ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U = Y ∖ K)}.
We use Y to witness the existential quantifier.
We use Ty to witness the existential quantifier.
We prove the intermediate claim HHausY: Hausdorff_space Y Ty.
We will prove topology_on Y Ty ∧ ∀x1 x2 : set, x1 ∈ Y → x2 ∈ Y → x1 ≠ x2 → ∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
We will prove topology_on Y Ty.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (locally_compact_topology X Tx Hlc).
We will prove Ty ⊆ 𝒫 Y ∧ Empty ∈ Ty ∧ Y ∈ Ty ∧ (∀UFam ∈ 𝒫 Ty, ⋃ UFam ∈ Ty) ∧ (∀U ∈ Ty, ∀V ∈ Ty, U ∩ V ∈ Ty).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We will prove Ty ⊆ 𝒫 Y.
Let U be given.
Assume HUty: U ∈ Ty.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) U HUty).
We will prove Empty ∈ Ty.
We prove the intermediate claim HEmptyPowY: Empty ∈ 𝒫 Y.
An exact proof term for the current goal is (Empty_In_Power Y).
We prove the intermediate claim HEmptyTx: Empty ∈ Tx.
An exact proof term for the current goal is (topology_has_empty X Tx HTx).
We prove the intermediate claim HpnotEmpty: p ∉ Empty.
An exact proof term for the current goal is (EmptyE p).
We prove the intermediate claim HPred: (p ∉ Empty ∧ Empty ∈ Tx) ∨ (p ∈ Empty ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ Empty = Y ∖ K).
An exact proof term for the current goal is (orIL (p ∉ Empty ∧ Empty ∈ Tx) (p ∈ Empty ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ Empty = Y ∖ K) (andI (p ∉ Empty) (Empty ∈ Tx) HpnotEmpty HEmptyTx)).
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) Empty HEmptyPowY HPred).
We will prove Y ∈ Ty.
We prove the intermediate claim HYpowY: Y ∈ 𝒫 Y.
An exact proof term for the current goal is (Self_In_Power Y).
We prove the intermediate claim HpY: p ∈ Y.
An exact proof term for the current goal is (binunionI2 X {p} p (SingI p)).
We prove the intermediate claim HEmptyComp: compact_space Empty (subspace_topology X Tx Empty).
An exact proof term for the current goal is (compact_empty_subspace X Tx HTx).
We prove the intermediate claim HPredY: (p ∉ Y ∧ Y ∈ Tx) ∨ (p ∈ Y ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ Y = Y ∖ K).
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HpY.
We use Empty to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HEmptyComp.
An exact proof term for the current goal is (Subq_Empty X).
rewrite the current goal using (setminus_Empty_eq Y) (from left to right).
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) Y HYpowY HPredY).
Let UFam be given.
Assume HUFamPow: UFam ∈ 𝒫 Ty.
We will prove ⋃ UFam ∈ Ty.
We prove the intermediate claim HUFamSub: UFam ⊆ Ty.
An exact proof term for the current goal is (PowerE Ty UFam HUFamPow).
We prove the intermediate claim HUnionPowY: ⋃ UFam ∈ 𝒫 Y.
Apply PowerI to the current goal.
Let y be given.
Assume HyU: y ∈ ⋃ UFam.
Apply (UnionE_impred UFam y HyU) to the current goal.
Let U be given.
Assume HyUin: y ∈ U.
Assume HUUFam: U ∈ UFam.
We prove the intermediate claim HUty: U ∈ Ty.
An exact proof term for the current goal is (HUFamSub U HUUFam).
We prove the intermediate claim HUpowY: U ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) U HUty).
We prove the intermediate claim HUsubY: U ⊆ Y.
An exact proof term for the current goal is (PowerE Y U HUpowY).
An exact proof term for the current goal is (HUsubY y HyUin).
Apply (xm (p ∈ ⋃ UFam)) to the current goal.
Assume HpUnion: p ∈ ⋃ UFam.
Set K to be the term Y ∖ ⋃ UFam.
We prove the intermediate claim HUnionEq: ⋃ UFam = Y ∖ K.
rewrite the current goal using (setminus_setminus_eq Y (⋃ UFam) (PowerE Y (⋃ UFam) HUnionPowY)) (from left to right).
Use reflexivity.
We prove the intermediate claim HKsubX: K ⊆ X.
Let y be given.
Assume HyK: y ∈ K.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (setminusE1 Y (⋃ UFam) y HyK).
Apply (binunionE X {p} y HyY (y ∈ X)) to the current goal.
Assume HyX: y ∈ X.
An exact proof term for the current goal is HyX.
Assume Hyp: y ∈ {p}.
We prove the intermediate claim Heq: y = p.
An exact proof term for the current goal is (SingE p y Hyp).
Apply FalseE to the current goal.
Apply (setminusE2 Y (⋃ UFam) y HyK) to the current goal.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HpUnion.
We prove the intermediate claim HPredUnion: (p ∉ ⋃ UFam ∧ ⋃ UFam ∈ Tx) ∨ (p ∈ ⋃ UFam ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ ⋃ UFam = Y ∖ K0).
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HpUnion.
We use K to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We will prove compact_space K (subspace_topology X Tx K).
Apply (UnionE_impred UFam p HpUnion) to the current goal.
Let U0 be given.
Assume HpU0: p ∈ U0.
Assume HU0Fam: U0 ∈ UFam.
We prove the intermediate claim HU0Ty: U0 ∈ Ty.
An exact proof term for the current goal is (HUFamSub U0 HU0Fam).
We prove the intermediate claim HU0prop: (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃Kp : set, compact_space Kp (subspace_topology X Tx Kp) ∧ Kp ⊆ X ∧ U0 = Y ∖ Kp).
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃Kp : set, compact_space Kp (subspace_topology X Tx Kp) ∧ Kp ⊆ X ∧ U0 = Y ∖ Kp)) U0 HU0Ty).
Apply HU0prop to the current goal.
Assume Hbad: p ∉ U0 ∧ U0 ∈ Tx.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((andEL (p ∉ U0) (U0 ∈ Tx) Hbad) HpU0).
Assume Hgood: p ∈ U0 ∧ ∃Kp : set, compact_space Kp (subspace_topology X Tx Kp) ∧ Kp ⊆ X ∧ U0 = Y ∖ Kp.
We prove the intermediate claim HexKp: ∃Kp : set, compact_space Kp (subspace_topology X Tx Kp) ∧ Kp ⊆ X ∧ U0 = Y ∖ Kp.
An exact proof term for the current goal is (andER (p ∈ U0) (∃Kp : set, compact_space Kp (subspace_topology X Tx Kp) ∧ Kp ⊆ X ∧ U0 = Y ∖ Kp) Hgood).
Apply HexKp to the current goal.
Let Kp be given.
Assume HKpPkg.
We prove the intermediate claim HKpLeft: compact_space Kp (subspace_topology X Tx Kp) ∧ Kp ⊆ X.
An exact proof term for the current goal is (andEL (compact_space Kp (subspace_topology X Tx Kp) ∧ Kp ⊆ X) (U0 = Y ∖ Kp) HKpPkg).
We prove the intermediate claim HKpComp: compact_space Kp (subspace_topology X Tx Kp).
An exact proof term for the current goal is (andEL (compact_space Kp (subspace_topology X Tx Kp)) (Kp ⊆ X) HKpLeft).
We prove the intermediate claim HKpSubX: Kp ⊆ X.
An exact proof term for the current goal is (andER (compact_space Kp (subspace_topology X Tx Kp)) (Kp ⊆ X) HKpLeft).
We prove the intermediate claim HU0eq: U0 = Y ∖ Kp.
An exact proof term for the current goal is (andER (compact_space Kp (subspace_topology X Tx Kp) ∧ Kp ⊆ X) (U0 = Y ∖ Kp) HKpPkg).
We prove the intermediate claim HKpSubY: Kp ⊆ Y.
Let y be given.
Assume HyKp: y ∈ Kp.
An exact proof term for the current goal is (binunionI1 X {p} y (HKpSubX y HyKp)).
We prove the intermediate claim HKsubKp: K ⊆ Kp.
Let y be given.
Assume HyK: y ∈ K.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (setminusE1 Y (⋃ UFam) y HyK).
We prove the intermediate claim HyNotUnion: y ∉ ⋃ UFam.
An exact proof term for the current goal is (setminusE2 Y (⋃ UFam) y HyK).
We prove the intermediate claim HyNotU0: y ∉ U0.
Assume HyU0: y ∈ U0.
An exact proof term for the current goal is (HyNotUnion (UnionI UFam y U0 HyU0 HU0Fam)).
We prove the intermediate claim HyNotYKp: y ∉ (Y ∖ Kp).
rewrite the current goal using HU0eq (from right to left).
An exact proof term for the current goal is HyNotU0.
We prove the intermediate claim HyInYYKp: y ∈ Y ∖ (Y ∖ Kp).
An exact proof term for the current goal is (setminusI Y (Y ∖ Kp) y HyY HyNotYKp).
rewrite the current goal using (setminus_setminus_eq Y Kp HKpSubY) (from right to left).
An exact proof term for the current goal is HyInYYKp.
Set TopKp to be the term subspace_topology X Tx Kp.
We prove the intermediate claim HTopKp: topology_on Kp TopKp.
An exact proof term for the current goal is (compact_space_topology Kp TopKp HKpComp).
We prove the intermediate claim HUopen: Kp ∖ K ∈ TopKp.
Set FamKp to be the term {W ∈ TopKp|∃U : set, U ∈ UFam ∧ W = U ∩ Kp}.
We prove the intermediate claim HFamKpPow: FamKp ∈ 𝒫 TopKp.
Apply PowerI to the current goal.
Let W be given.
Assume HW: W ∈ FamKp.
An exact proof term for the current goal is (SepE1 TopKp (λW0 : set ⇒ ∃U : set, U ∈ UFam ∧ W0 = U ∩ Kp) W HW).
We prove the intermediate claim HUnionFamKpTop: ⋃ FamKp ∈ TopKp.
An exact proof term for the current goal is (topology_union_closed_pow Kp TopKp FamKp HTopKp HFamKpPow).
We prove the intermediate claim HeqUnion: Kp ∖ K = ⋃ FamKp.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ Kp ∖ K.
We prove the intermediate claim HyKp: y ∈ Kp.
An exact proof term for the current goal is (setminusE1 Kp K y Hy).
We prove the intermediate claim HyNotK: y ∉ K.
An exact proof term for the current goal is (setminusE2 Kp K y Hy).
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (HKpSubY y HyKp).
We prove the intermediate claim HyUnion: y ∈ ⋃ UFam.
Apply (xm (y ∈ ⋃ UFam)) to the current goal.
Assume HyU.
An exact proof term for the current goal is HyU.
Assume HyNotUnion: ¬ (y ∈ ⋃ UFam).
We prove the intermediate claim HyK: y ∈ K.
An exact proof term for the current goal is (setminusI Y (⋃ UFam) y HyY HyNotUnion).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HyNotK HyK).
Apply (UnionE_impred UFam y HyUnion) to the current goal.
Let U be given.
Assume HyU: y ∈ U.
Assume HUUFam: U ∈ UFam.
Set W to be the term U ∩ Kp.
We prove the intermediate claim HyW: y ∈ W.
An exact proof term for the current goal is (binintersectI U Kp y HyU HyKp).
We prove the intermediate claim HWTop: W ∈ TopKp.
We prove the intermediate claim HWpow: W ∈ 𝒫 Kp.
Apply PowerI to the current goal.
Let z be given.
Assume HzW: z ∈ W.
An exact proof term for the current goal is (binintersectE2 U Kp z HzW).
We prove the intermediate claim HUty: U ∈ Ty.
An exact proof term for the current goal is (HUFamSub U HUUFam).
We prove the intermediate claim HUprop: (p ∉ U ∧ U ∈ Tx) ∨ (p ∈ U ∧ ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U = Y ∖ K1).
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U0 = Y ∖ K1)) U HUty).
Apply HUprop to the current goal.
Assume Hcase: p ∉ U ∧ U ∈ Tx.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andER (p ∉ U) (U ∈ Tx) Hcase).
We prove the intermediate claim HexV: ∃V ∈ Tx, W = V ∩ Kp.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUinTx.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 Kp) (λW0 : set ⇒ ∃V ∈ Tx, W0 = V ∩ Kp) W HWpow HexV).
Assume Hcase: p ∈ U ∧ ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U = Y ∖ K1.
We prove the intermediate claim HexK1: ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U = Y ∖ K1.
An exact proof term for the current goal is (andER (p ∈ U) (∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U = Y ∖ K1) Hcase).
Apply HexK1 to the current goal.
Let K1 be given.
Assume HK1pkg.
We prove the intermediate claim HK1left: compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X.
An exact proof term for the current goal is (andEL (compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X) (U = Y ∖ K1) HK1pkg).
We prove the intermediate claim HK1comp: compact_space K1 (subspace_topology X Tx K1).
An exact proof term for the current goal is (andEL (compact_space K1 (subspace_topology X Tx K1)) (K1 ⊆ X) HK1left).
We prove the intermediate claim HK1subX: K1 ⊆ X.
An exact proof term for the current goal is (andER (compact_space K1 (subspace_topology X Tx K1)) (K1 ⊆ X) HK1left).
We prove the intermediate claim HUeq: U = Y ∖ K1.
An exact proof term for the current goal is (andER (compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X) (U = Y ∖ K1) HK1pkg).
We prove the intermediate claim HK1closed: closed_in X Tx K1.
An exact proof term for the current goal is (Hausdorff_compact_sets_closed X Tx K1 HH HK1subX HK1comp).
We prove the intermediate claim Hop: open_in X Tx (X ∖ K1).
An exact proof term for the current goal is (open_of_closed_complement X Tx K1 HK1closed).
We prove the intermediate claim HVinTx: (X ∖ K1) ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ K1) Hop).
We prove the intermediate claim HeqW: W = (X ∖ K1) ∩ Kp.
rewrite the current goal using HUeq (from left to right).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (Y ∖ K1) ∩ Kp.
We prove the intermediate claim HxYK1: x ∈ Y ∖ K1.
An exact proof term for the current goal is (binintersectE1 (Y ∖ K1) Kp x Hx).
We prove the intermediate claim HxKp: x ∈ Kp.
An exact proof term for the current goal is (binintersectE2 (Y ∖ K1) Kp x Hx).
We prove the intermediate claim HxnotK1: x ∉ K1.
An exact proof term for the current goal is (setminusE2 Y K1 x HxYK1).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HKpSubX x HxKp).
We prove the intermediate claim HxXK1: x ∈ X ∖ K1.
An exact proof term for the current goal is (setminusI X K1 x HxX HxnotK1).
Apply binintersectI to the current goal.
An exact proof term for the current goal is HxXK1.
An exact proof term for the current goal is HxKp.
Let x be given.
Assume Hx: x ∈ (X ∖ K1) ∩ Kp.
We prove the intermediate claim HxXK1: x ∈ X ∖ K1.
An exact proof term for the current goal is (binintersectE1 (X ∖ K1) Kp x Hx).
We prove the intermediate claim HxKp: x ∈ Kp.
An exact proof term for the current goal is (binintersectE2 (X ∖ K1) Kp x Hx).
We prove the intermediate claim HxnotK1: x ∉ K1.
An exact proof term for the current goal is (setminusE2 X K1 x HxXK1).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (HKpSubY x HxKp).
We prove the intermediate claim HxYK1: x ∈ Y ∖ K1.
An exact proof term for the current goal is (setminusI Y K1 x HxY HxnotK1).
Apply binintersectI to the current goal.
An exact proof term for the current goal is HxYK1.
An exact proof term for the current goal is HxKp.
We prove the intermediate claim HexV: ∃V ∈ Tx, W = V ∩ Kp.
We use (X ∖ K1) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVinTx.
An exact proof term for the current goal is HeqW.
An exact proof term for the current goal is (SepI (𝒫 Kp) (λW0 : set ⇒ ∃V ∈ Tx, W0 = V ∩ Kp) W HWpow HexV).
We prove the intermediate claim HWFam: W ∈ FamKp.
We prove the intermediate claim HexU: ∃U0 : set, U0 ∈ UFam ∧ W = U0 ∩ Kp.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUUFam.
Use reflexivity.
An exact proof term for the current goal is (SepI TopKp (λW0 : set ⇒ ∃U0 : set, U0 ∈ UFam ∧ W0 = U0 ∩ Kp) W HWTop HexU).
An exact proof term for the current goal is (UnionI FamKp y W HyW HWFam).
Let y be given.
Assume Hy: y ∈ ⋃ FamKp.
Apply (UnionE_impred FamKp y Hy) to the current goal.
Let W be given.
Assume HyW: y ∈ W.
Assume HWFam: W ∈ FamKp.
We prove the intermediate claim HexU: ∃U : set, U ∈ UFam ∧ W = U ∩ Kp.
An exact proof term for the current goal is (SepE2 TopKp (λW0 : set ⇒ ∃U : set, U ∈ UFam ∧ W0 = U ∩ Kp) W HWFam).
Apply HexU to the current goal.
Let U be given.
Assume HUand.
We prove the intermediate claim HUUFam: U ∈ UFam.
An exact proof term for the current goal is (andEL (U ∈ UFam) (W = U ∩ Kp) HUand).
We prove the intermediate claim HWeq: W = U ∩ Kp.
An exact proof term for the current goal is (andER (U ∈ UFam) (W = U ∩ Kp) HUand).
We prove the intermediate claim HyUKp: y ∈ U ∩ Kp.
rewrite the current goal using HWeq (from right to left).
An exact proof term for the current goal is HyW.
We prove the intermediate claim HyKp: y ∈ Kp.
An exact proof term for the current goal is (binintersectE2 U Kp y HyUKp).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U Kp y HyUKp).
We prove the intermediate claim HyUnionUFam: y ∈ ⋃ UFam.
An exact proof term for the current goal is (UnionI UFam y U HyU HUUFam).
We prove the intermediate claim HyNotK: y ∉ K.
Assume HyK: y ∈ K.
We prove the intermediate claim HyNotUnion: y ∉ ⋃ UFam.
An exact proof term for the current goal is (setminusE2 Y (⋃ UFam) y HyK).
An exact proof term for the current goal is (HyNotUnion HyUnionUFam).
An exact proof term for the current goal is (setminusI Kp K y HyKp HyNotK).
rewrite the current goal using HeqUnion (from left to right).
An exact proof term for the current goal is HUnionFamKpTop.
We prove the intermediate claim HKclosedTmp: closed_in Kp TopKp (Kp ∖ (Kp ∖ K)).
An exact proof term for the current goal is (closed_of_open_complement Kp TopKp (Kp ∖ K) HTopKp HUopen).
We prove the intermediate claim HKclosed: closed_in Kp TopKp K.
rewrite the current goal using (setminus_setminus_eq Kp K HKsubKp) (from right to left).
An exact proof term for the current goal is HKclosedTmp.
We prove the intermediate claim HKcompSub: compact_space K (subspace_topology Kp TopKp K).
An exact proof term for the current goal is (closed_subspace_compact Kp TopKp K HKpComp HKclosed).
We prove the intermediate claim HeqTop: subspace_topology Kp TopKp K = subspace_topology X Tx K.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx Kp K HTx HKpSubX HKsubKp).
rewrite the current goal using HeqTop (from right to left).
An exact proof term for the current goal is HKcompSub.
An exact proof term for the current goal is HKsubX.
An exact proof term for the current goal is HUnionEq.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 = Y ∖ K0)) (⋃ UFam) HUnionPowY HPredUnion).
Assume HpNotUnion: ¬ (p ∈ ⋃ UFam).
We prove the intermediate claim HpNotUnion2: p ∉ ⋃ UFam.
An exact proof term for the current goal is HpNotUnion.
We prove the intermediate claim HUFamTx: UFam ⊆ Tx.
Let U be given.
Assume HUUFam: U ∈ UFam.
We prove the intermediate claim HUty: U ∈ Ty.
An exact proof term for the current goal is (HUFamSub U HUUFam).
We prove the intermediate claim HUprop: (p ∉ U ∧ U ∈ Tx) ∨ (p ∈ U ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U = Y ∖ K).
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) U HUty).
Apply HUprop to the current goal.
Assume Hcase: p ∉ U ∧ U ∈ Tx.
An exact proof term for the current goal is (andER (p ∉ U) (U ∈ Tx) Hcase).
Assume Hcase: p ∈ U ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U = Y ∖ K.
Apply FalseE to the current goal.
We prove the intermediate claim HpU: p ∈ U.
An exact proof term for the current goal is (andEL (p ∈ U) (∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U = Y ∖ K) Hcase).
Apply HpNotUnion to the current goal.
An exact proof term for the current goal is (UnionI UFam p U HpU HUUFam).
We prove the intermediate claim HUnionTx: ⋃ UFam ∈ Tx.
An exact proof term for the current goal is (topology_union_closed X Tx UFam HTx HUFamTx).
We prove the intermediate claim HPredUnion: (p ∉ ⋃ UFam ∧ ⋃ UFam ∈ Tx) ∨ (p ∈ ⋃ UFam ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ ⋃ UFam = Y ∖ K0).
An exact proof term for the current goal is (orIL (p ∉ ⋃ UFam ∧ ⋃ UFam ∈ Tx) (p ∈ ⋃ UFam ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ ⋃ UFam = Y ∖ K0) (andI (p ∉ ⋃ UFam) (⋃ UFam ∈ Tx) HpNotUnion2 HUnionTx)).
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 = Y ∖ K0)) (⋃ UFam) HUnionPowY HPredUnion).
Let U be given.
Assume HUty: U ∈ Ty.
Let V be given.
Assume HVty: V ∈ Ty.
We will prove U ∩ V ∈ Ty.
We prove the intermediate claim HUpowY: U ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) U HUty).
We prove the intermediate claim HVpowY: V ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) V HVty).
We prove the intermediate claim HUVpowY: U ∩ V ∈ 𝒫 Y.
Apply PowerI to the current goal.
Let y be given.
Assume HyUV: y ∈ U ∩ V.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U V y HyUV).
We prove the intermediate claim HUsubY: U ⊆ Y.
An exact proof term for the current goal is (PowerE Y U HUpowY).
An exact proof term for the current goal is (HUsubY y HyU).
We prove the intermediate claim HUprop: (p ∉ U ∧ U ∈ Tx) ∨ (p ∈ U ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U = Y ∖ K).
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) U HUty).
We prove the intermediate claim HVprop: (p ∉ V ∧ V ∈ Tx) ∨ (p ∈ V ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ V = Y ∖ K).
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) V HVty).
Apply HUprop to the current goal.
Assume HcaseU: p ∉ U ∧ U ∈ Tx.
We prove the intermediate claim HUpnot: p ∉ U.
An exact proof term for the current goal is (andEL (p ∉ U) (U ∈ Tx) HcaseU).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andER (p ∉ U) (U ∈ Tx) HcaseU).
Apply HVprop to the current goal.
Assume HcaseV: p ∉ V ∧ V ∈ Tx.
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (andER (p ∉ V) (V ∈ Tx) HcaseV).
We prove the intermediate claim HUVinTx: U ∩ V ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx U V HTx HUinTx HVinTx).
We prove the intermediate claim HpnotUV: p ∉ U ∩ V.
Assume HpUV: p ∈ U ∩ V.
We prove the intermediate claim HpU: p ∈ U.
An exact proof term for the current goal is (binintersectE1 U V p HpUV).
An exact proof term for the current goal is (HUpnot HpU).
We prove the intermediate claim HPredUV: (p ∉ U ∩ V ∧ U ∩ V ∈ Tx) ∨ (p ∈ U ∩ V ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U ∩ V = Y ∖ K0).
An exact proof term for the current goal is (orIL (p ∉ U ∩ V ∧ U ∩ V ∈ Tx) (p ∈ U ∩ V ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U ∩ V = Y ∖ K0) (andI (p ∉ U ∩ V) (U ∩ V ∈ Tx) HpnotUV HUVinTx)).
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 = Y ∖ K0)) (U ∩ V) HUVpowY HPredUV).
Assume HcaseV: p ∈ V ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ V = Y ∖ K.
We prove the intermediate claim HexK: ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ V = Y ∖ K.
An exact proof term for the current goal is (andER (p ∈ V) (∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ V = Y ∖ K) HcaseV).
Apply HexK to the current goal.
Let K be given.
Assume HKpkg.
We prove the intermediate claim HKleft: compact_space K (subspace_topology X Tx K) ∧ K ⊆ X.
An exact proof term for the current goal is (andEL (compact_space K (subspace_topology X Tx K) ∧ K ⊆ X) (V = Y ∖ K) HKpkg).
We prove the intermediate claim HKcomp: compact_space K (subspace_topology X Tx K).
An exact proof term for the current goal is (andEL (compact_space K (subspace_topology X Tx K)) (K ⊆ X) HKleft).
We prove the intermediate claim HKsubX: K ⊆ X.
An exact proof term for the current goal is (andER (compact_space K (subspace_topology X Tx K)) (K ⊆ X) HKleft).
We prove the intermediate claim HVeq: V = Y ∖ K.
An exact proof term for the current goal is (andER (compact_space K (subspace_topology X Tx K) ∧ K ⊆ X) (V = Y ∖ K) HKpkg).
We prove the intermediate claim HclK: closed_in X Tx K.
An exact proof term for the current goal is (Hausdorff_compact_sets_closed X Tx K HH HKsubX HKcomp).
We prove the intermediate claim HopK: open_in X Tx (X ∖ K).
An exact proof term for the current goal is (open_of_closed_complement X Tx K HclK).
We prove the intermediate claim HUVinTx: U ∩ (X ∖ K) ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx U (X ∖ K) HTx HUinTx (open_in_elem X Tx (X ∖ K) HopK)).
We prove the intermediate claim HUVeq: U ∩ V = U ∩ (X ∖ K).
rewrite the current goal using HVeq (from left to right).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ U ∩ (Y ∖ K).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U (Y ∖ K) x Hx).
We prove the intermediate claim HxYK: x ∈ Y ∖ K.
An exact proof term for the current goal is (binintersectE2 U (Y ∖ K) x Hx).
We prove the intermediate claim HxnotK: x ∉ K.
An exact proof term for the current goal is (setminusE2 Y K x HxYK).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is ((topology_elem_subset X Tx U HTx HUinTx) x HxU).
We prove the intermediate claim HxXK: x ∈ X ∖ K.
An exact proof term for the current goal is (setminusI X K x HxX HxnotK).
An exact proof term for the current goal is (binintersectI U (X ∖ K) x HxU HxXK).
Let x be given.
Assume Hx: x ∈ U ∩ (X ∖ K).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U (X ∖ K) x Hx).
We prove the intermediate claim HxXK: x ∈ X ∖ K.
An exact proof term for the current goal is (binintersectE2 U (X ∖ K) x Hx).
We prove the intermediate claim HxnotK: x ∉ K.
An exact proof term for the current goal is (setminusE2 X K x HxXK).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binunionI1 X {p} x ((topology_elem_subset X Tx U HTx HUinTx) x HxU)).
We prove the intermediate claim HxYK: x ∈ Y ∖ K.
An exact proof term for the current goal is (setminusI Y K x HxY HxnotK).
An exact proof term for the current goal is (binintersectI U (Y ∖ K) x HxU HxYK).
We prove the intermediate claim HpnotUV: p ∉ U ∩ V.
Assume HpUV: p ∈ U ∩ V.
We prove the intermediate claim HpU: p ∈ U.
An exact proof term for the current goal is (binintersectE1 U V p HpUV).
An exact proof term for the current goal is (HUpnot HpU).
We prove the intermediate claim HPredUV: (p ∉ U ∩ V ∧ U ∩ V ∈ Tx) ∨ (p ∈ U ∩ V ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U ∩ V = Y ∖ K0).
We prove the intermediate claim HUVinTx2: U ∩ V ∈ Tx.
rewrite the current goal using HUVeq (from left to right).
An exact proof term for the current goal is HUVinTx.
An exact proof term for the current goal is (orIL (p ∉ U ∩ V ∧ U ∩ V ∈ Tx) (p ∈ U ∩ V ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U ∩ V = Y ∖ K0) (andI (p ∉ U ∩ V) (U ∩ V ∈ Tx) HpnotUV HUVinTx2)).
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 = Y ∖ K0)) (U ∩ V) HUVpowY HPredUV).
Assume HcaseU: p ∈ U ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U = Y ∖ K.
We prove the intermediate claim HexK1: ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U = Y ∖ K1.
An exact proof term for the current goal is (andER (p ∈ U) (∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U = Y ∖ K1) HcaseU).
Apply HexK1 to the current goal.
Let K1 be given.
Assume HK1pkg.
We prove the intermediate claim HK1left: compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X.
An exact proof term for the current goal is (andEL (compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X) (U = Y ∖ K1) HK1pkg).
We prove the intermediate claim HK1comp: compact_space K1 (subspace_topology X Tx K1).
An exact proof term for the current goal is (andEL (compact_space K1 (subspace_topology X Tx K1)) (K1 ⊆ X) HK1left).
We prove the intermediate claim HK1subX: K1 ⊆ X.
An exact proof term for the current goal is (andER (compact_space K1 (subspace_topology X Tx K1)) (K1 ⊆ X) HK1left).
We prove the intermediate claim HUeq: U = Y ∖ K1.
An exact proof term for the current goal is (andER (compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X) (U = Y ∖ K1) HK1pkg).
We prove the intermediate claim HclK1: closed_in X Tx K1.
An exact proof term for the current goal is (Hausdorff_compact_sets_closed X Tx K1 HH HK1subX HK1comp).
We prove the intermediate claim HopK1: open_in X Tx (X ∖ K1).
An exact proof term for the current goal is (open_of_closed_complement X Tx K1 HclK1).
We prove the intermediate claim HXK1inTx: (X ∖ K1) ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ K1) HopK1).
Apply HVprop to the current goal.
Assume HcaseV: p ∉ V ∧ V ∈ Tx.
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (andER (p ∉ V) (V ∈ Tx) HcaseV).
We prove the intermediate claim HVsubX: V ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V HTx HVinTx).
We prove the intermediate claim HUVinTx: V ∩ (X ∖ K1) ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx V (X ∖ K1) HTx HVinTx HXK1inTx).
We prove the intermediate claim HpnotUV: p ∉ U ∩ V.
Assume HpUV: p ∈ U ∩ V.
We prove the intermediate claim HpV: p ∈ V.
An exact proof term for the current goal is (binintersectE2 U V p HpUV).
An exact proof term for the current goal is ((andEL (p ∉ V) (V ∈ Tx) HcaseV) HpV).
We prove the intermediate claim HeqUV: U ∩ V = V ∩ (X ∖ K1).
rewrite the current goal using HUeq (from left to right).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (Y ∖ K1) ∩ V.
We prove the intermediate claim HxYK1: x ∈ Y ∖ K1.
An exact proof term for the current goal is (binintersectE1 (Y ∖ K1) V x Hx).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE2 (Y ∖ K1) V x Hx).
We prove the intermediate claim HxnotK1: x ∉ K1.
An exact proof term for the current goal is (setminusE2 Y K1 x HxYK1).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HVsubX x HxV).
We prove the intermediate claim HxXK1: x ∈ X ∖ K1.
An exact proof term for the current goal is (setminusI X K1 x HxX HxnotK1).
An exact proof term for the current goal is (binintersectI V (X ∖ K1) x HxV HxXK1).
Let x be given.
Assume Hx: x ∈ V ∩ (X ∖ K1).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE1 V (X ∖ K1) x Hx).
We prove the intermediate claim HxXK1: x ∈ X ∖ K1.
An exact proof term for the current goal is (binintersectE2 V (X ∖ K1) x Hx).
We prove the intermediate claim HxnotK1: x ∉ K1.
An exact proof term for the current goal is (setminusE2 X K1 x HxXK1).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binunionI1 X {p} x (HVsubX x HxV)).
We prove the intermediate claim HxYK1: x ∈ Y ∖ K1.
An exact proof term for the current goal is (setminusI Y K1 x HxY HxnotK1).
An exact proof term for the current goal is (binintersectI (Y ∖ K1) V x HxYK1 HxV).
We prove the intermediate claim HPredUV: (p ∉ U ∩ V ∧ U ∩ V ∈ Tx) ∨ (p ∈ U ∩ V ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U ∩ V = Y ∖ K0).
We prove the intermediate claim HUVinTx2: U ∩ V ∈ Tx.
rewrite the current goal using HeqUV (from left to right).
An exact proof term for the current goal is HUVinTx.
An exact proof term for the current goal is (orIL (p ∉ U ∩ V ∧ U ∩ V ∈ Tx) (p ∈ U ∩ V ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U ∩ V = Y ∖ K0) (andI (p ∉ U ∩ V) (U ∩ V ∈ Tx) HpnotUV HUVinTx2)).
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 = Y ∖ K0)) (U ∩ V) HUVpowY HPredUV).
Assume HcaseV: p ∈ V ∧ ∃K2 : set, compact_space K2 (subspace_topology X Tx K2) ∧ K2 ⊆ X ∧ V = Y ∖ K2.
We prove the intermediate claim HexK2: ∃K2 : set, compact_space K2 (subspace_topology X Tx K2) ∧ K2 ⊆ X ∧ V = Y ∖ K2.
An exact proof term for the current goal is (andER (p ∈ V) (∃K2 : set, compact_space K2 (subspace_topology X Tx K2) ∧ K2 ⊆ X ∧ V = Y ∖ K2) HcaseV).
Apply HexK2 to the current goal.
Let K2 be given.
Assume HK2pkg.
We prove the intermediate claim HK2left: compact_space K2 (subspace_topology X Tx K2) ∧ K2 ⊆ X.
An exact proof term for the current goal is (andEL (compact_space K2 (subspace_topology X Tx K2) ∧ K2 ⊆ X) (V = Y ∖ K2) HK2pkg).
We prove the intermediate claim HK2comp: compact_space K2 (subspace_topology X Tx K2).
An exact proof term for the current goal is (andEL (compact_space K2 (subspace_topology X Tx K2)) (K2 ⊆ X) HK2left).
We prove the intermediate claim HK2subX: K2 ⊆ X.
An exact proof term for the current goal is (andER (compact_space K2 (subspace_topology X Tx K2)) (K2 ⊆ X) HK2left).
We prove the intermediate claim HVeq: V = Y ∖ K2.
An exact proof term for the current goal is (andER (compact_space K2 (subspace_topology X Tx K2) ∧ K2 ⊆ X) (V = Y ∖ K2) HK2pkg).
Set K12 to be the term K1 ∪ K2.
We prove the intermediate claim HK12subX: K12 ⊆ X.
Let x be given.
Assume Hx: x ∈ K12.
Apply (binunionE K1 K2 x Hx (x ∈ X)) to the current goal.
Assume HxK1: x ∈ K1.
An exact proof term for the current goal is (HK1subX x HxK1).
Assume HxK2: x ∈ K2.
An exact proof term for the current goal is (HK2subX x HxK2).
We prove the intermediate claim HK12comp: compact_space K12 (subspace_topology X Tx K12).
We prove the intermediate claim HK1equiv: (compact_space K1 (subspace_topology X Tx K1) ↔ ∀Fam : set, (Fam ⊆ Tx ∧ K1 ⊆ ⋃ Fam) → has_finite_subcover K1 Tx Fam).
An exact proof term for the current goal is (compact_subspace_via_ambient_covers X Tx K1 HTx HK1subX).
We prove the intermediate claim HK2equiv: (compact_space K2 (subspace_topology X Tx K2) ↔ ∀Fam : set, (Fam ⊆ Tx ∧ K2 ⊆ ⋃ Fam) → has_finite_subcover K2 Tx Fam).
An exact proof term for the current goal is (compact_subspace_via_ambient_covers X Tx K2 HTx HK2subX).
We prove the intermediate claim HK1amb: ∀Fam : set, (Fam ⊆ Tx ∧ K1 ⊆ ⋃ Fam) → has_finite_subcover K1 Tx Fam.
An exact proof term for the current goal is (iffEL (compact_space K1 (subspace_topology X Tx K1)) (∀Fam : set, (Fam ⊆ Tx ∧ K1 ⊆ ⋃ Fam) → has_finite_subcover K1 Tx Fam) HK1equiv HK1comp).
We prove the intermediate claim HK2amb: ∀Fam : set, (Fam ⊆ Tx ∧ K2 ⊆ ⋃ Fam) → has_finite_subcover K2 Tx Fam.
An exact proof term for the current goal is (iffEL (compact_space K2 (subspace_topology X Tx K2)) (∀Fam : set, (Fam ⊆ Tx ∧ K2 ⊆ ⋃ Fam) → has_finite_subcover K2 Tx Fam) HK2equiv HK2comp).
We prove the intermediate claim HK12equiv: (compact_space K12 (subspace_topology X Tx K12) ↔ ∀Fam : set, (Fam ⊆ Tx ∧ K12 ⊆ ⋃ Fam) → has_finite_subcover K12 Tx Fam).
An exact proof term for the current goal is (compact_subspace_via_ambient_covers X Tx K12 HTx HK12subX).
Apply (iffER (compact_space K12 (subspace_topology X Tx K12)) (∀Fam : set, (Fam ⊆ Tx ∧ K12 ⊆ ⋃ Fam) → has_finite_subcover K12 Tx Fam) HK12equiv) to the current goal.
Let Fam be given.
Assume Hcov: Fam ⊆ Tx ∧ K12 ⊆ ⋃ Fam.
We prove the intermediate claim HFsub: Fam ⊆ Tx.
An exact proof term for the current goal is (andEL (Fam ⊆ Tx) (K12 ⊆ ⋃ Fam) Hcov).
We prove the intermediate claim HK12cov: K12 ⊆ ⋃ Fam.
An exact proof term for the current goal is (andER (Fam ⊆ Tx) (K12 ⊆ ⋃ Fam) Hcov).
We prove the intermediate claim HK1cov: K1 ⊆ ⋃ Fam.
Let x be given.
Assume HxK1: x ∈ K1.
An exact proof term for the current goal is (HK12cov x (binunionI1 K1 K2 x HxK1)).
We prove the intermediate claim HK2cov: K2 ⊆ ⋃ Fam.
Let x be given.
Assume HxK2: x ∈ K2.
An exact proof term for the current goal is (HK12cov x (binunionI2 K1 K2 x HxK2)).
We prove the intermediate claim Hfin1: has_finite_subcover K1 Tx Fam.
An exact proof term for the current goal is (HK1amb Fam (andI (Fam ⊆ Tx) (K1 ⊆ ⋃ Fam) HFsub HK1cov)).
We prove the intermediate claim Hfin2: has_finite_subcover K2 Tx Fam.
An exact proof term for the current goal is (HK2amb Fam (andI (Fam ⊆ Tx) (K2 ⊆ ⋃ Fam) HFsub HK2cov)).
Apply Hfin1 to the current goal.
Let G1 be given.
Assume HG1.
Apply Hfin2 to the current goal.
Let G2 be given.
Assume HG2.
Set G to be the term G1 ∪ G2.
Apply (has_finite_subcoverI K12 Tx Fam G) to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ G.
Apply (binunionE G1 G2 U0 HU0 (U0 ∈ Fam)) to the current goal.
Assume HU0G1: U0 ∈ G1.
We prove the intermediate claim HG1left: G1 ⊆ Fam ∧ finite G1.
An exact proof term for the current goal is (andEL (G1 ⊆ Fam ∧ finite G1) (K1 ⊆ ⋃ G1) HG1).
We prove the intermediate claim HG1sub: G1 ⊆ Fam.
An exact proof term for the current goal is (andEL (G1 ⊆ Fam) (finite G1) HG1left).
An exact proof term for the current goal is (HG1sub U0 HU0G1).
Assume HU0G2: U0 ∈ G2.
We prove the intermediate claim HG2left: G2 ⊆ Fam ∧ finite G2.
An exact proof term for the current goal is (andEL (G2 ⊆ Fam ∧ finite G2) (K2 ⊆ ⋃ G2) HG2).
We prove the intermediate claim HG2sub: G2 ⊆ Fam.
An exact proof term for the current goal is (andEL (G2 ⊆ Fam) (finite G2) HG2left).
An exact proof term for the current goal is (HG2sub U0 HU0G2).
We prove the intermediate claim HG1left: G1 ⊆ Fam ∧ finite G1.
An exact proof term for the current goal is (andEL (G1 ⊆ Fam ∧ finite G1) (K1 ⊆ ⋃ G1) HG1).
We prove the intermediate claim HG2left: G2 ⊆ Fam ∧ finite G2.
An exact proof term for the current goal is (andEL (G2 ⊆ Fam ∧ finite G2) (K2 ⊆ ⋃ G2) HG2).
An exact proof term for the current goal is (binunion_finite G1 (andER (G1 ⊆ Fam) (finite G1) HG1left) G2 (andER (G2 ⊆ Fam) (finite G2) HG2left)).
Let x be given.
Assume HxK12: x ∈ K12.
Apply (binunionE K1 K2 x HxK12 (x ∈ ⋃ G)) to the current goal.
Assume HxK1: x ∈ K1.
We prove the intermediate claim HG1cov: K1 ⊆ ⋃ G1.
An exact proof term for the current goal is (andER (G1 ⊆ Fam ∧ finite G1) (K1 ⊆ ⋃ G1) HG1).
We prove the intermediate claim Hcov1: x ∈ ⋃ G1.
An exact proof term for the current goal is (HG1cov x HxK1).
Apply (UnionE_impred G1 x Hcov1) to the current goal.
Let U0 be given.
Assume HxU0: x ∈ U0.
Assume HU0G1: U0 ∈ G1.
An exact proof term for the current goal is (UnionI G x U0 HxU0 (binunionI1 G1 G2 U0 HU0G1)).
Assume HxK2: x ∈ K2.
We prove the intermediate claim HG2cov: K2 ⊆ ⋃ G2.
An exact proof term for the current goal is (andER (G2 ⊆ Fam ∧ finite G2) (K2 ⊆ ⋃ G2) HG2).
We prove the intermediate claim Hcov2: x ∈ ⋃ G2.
An exact proof term for the current goal is (HG2cov x HxK2).
Apply (UnionE_impred G2 x Hcov2) to the current goal.
Let U0 be given.
Assume HxU0: x ∈ U0.
Assume HU0G2: U0 ∈ G2.
An exact proof term for the current goal is (UnionI G x U0 HxU0 (binunionI2 G1 G2 U0 HU0G2)).
We prove the intermediate claim HpUV: p ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V p (andEL (p ∈ U) (∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U = Y ∖ K1) HcaseU) (andEL (p ∈ V) (∃K2 : set, compact_space K2 (subspace_topology X Tx K2) ∧ K2 ⊆ X ∧ V = Y ∖ K2) HcaseV)).
We prove the intermediate claim HeqUV: U ∩ V = Y ∖ K12.
rewrite the current goal using HUeq (from left to right).
rewrite the current goal using HVeq (from left to right).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (Y ∖ K1) ∩ (Y ∖ K2).
We prove the intermediate claim HxYK1: x ∈ Y ∖ K1.
An exact proof term for the current goal is (binintersectE1 (Y ∖ K1) (Y ∖ K2) x Hx).
We prove the intermediate claim HxYK2: x ∈ Y ∖ K2.
An exact proof term for the current goal is (binintersectE2 (Y ∖ K1) (Y ∖ K2) x Hx).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (setminusE1 Y K1 x HxYK1).
We prove the intermediate claim HxnotK1: x ∉ K1.
An exact proof term for the current goal is (setminusE2 Y K1 x HxYK1).
We prove the intermediate claim HxnotK2: x ∉ K2.
An exact proof term for the current goal is (setminusE2 Y K2 x HxYK2).
We prove the intermediate claim HxnotK12: x ∉ K12.
Assume HxK12: x ∈ K12.
Apply (binunionE K1 K2 x HxK12 False) to the current goal.
Assume HxK1: x ∈ K1.
An exact proof term for the current goal is (HxnotK1 HxK1).
Assume HxK2: x ∈ K2.
An exact proof term for the current goal is (HxnotK2 HxK2).
An exact proof term for the current goal is (setminusI Y K12 x HxY HxnotK12).
Let x be given.
Assume Hx: x ∈ Y ∖ K12.
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (setminusE1 Y K12 x Hx).
We prove the intermediate claim HxnotK12: x ∉ K12.
An exact proof term for the current goal is (setminusE2 Y K12 x Hx).
We prove the intermediate claim HxnotK1: x ∉ K1.
Assume HxK1: x ∈ K1.
Apply HxnotK12 to the current goal.
An exact proof term for the current goal is (binunionI1 K1 K2 x HxK1).
We prove the intermediate claim HxnotK2: x ∉ K2.
Assume HxK2: x ∈ K2.
Apply HxnotK12 to the current goal.
An exact proof term for the current goal is (binunionI2 K1 K2 x HxK2).
We prove the intermediate claim HxYK1: x ∈ Y ∖ K1.
An exact proof term for the current goal is (setminusI Y K1 x HxY HxnotK1).
We prove the intermediate claim HxYK2: x ∈ Y ∖ K2.
An exact proof term for the current goal is (setminusI Y K2 x HxY HxnotK2).
An exact proof term for the current goal is (binintersectI (Y ∖ K1) (Y ∖ K2) x HxYK1 HxYK2).
We prove the intermediate claim HPredUV: (p ∉ U ∩ V ∧ U ∩ V ∈ Tx) ∨ (p ∈ U ∩ V ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U ∩ V = Y ∖ K0).
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HpUV.
We use K12 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HK12comp.
An exact proof term for the current goal is HK12subX.
An exact proof term for the current goal is HeqUV.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 = Y ∖ K0)) (U ∩ V) HUVpowY HPredUV).
Let x1 and x2 be given.
Assume Hx1Y: x1 ∈ Y.
Assume Hx2Y: x2 ∈ Y.
Assume Hneq: x1 ≠ x2.
We will prove ∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
Apply (binunionE X {p} x1 Hx1Y (∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty)) to the current goal.
Assume Hx1X: x1 ∈ X.
Apply (binunionE X {p} x2 Hx2Y (∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty)) to the current goal.
Assume Hx2X: x2 ∈ X.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (Hausdorff_space_topology X Tx HH).
Apply (Hausdorff_space_separation X Tx x1 x2 HH Hx1X Hx2X Hneq) to the current goal.
Let U be given.
Assume HexV.
Apply HexV to the current goal.
Let V be given.
Assume HUV.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
We prove the intermediate claim HUV1: ((U ∈ Tx ∧ V ∈ Tx) ∧ x1 ∈ U) ∧ x2 ∈ V.
An exact proof term for the current goal is (andEL (((U ∈ Tx ∧ V ∈ Tx) ∧ x1 ∈ U) ∧ x2 ∈ V) (U ∩ V = Empty) HUV).
We prove the intermediate claim HUVempty: U ∩ V = Empty.
An exact proof term for the current goal is (andER (((U ∈ Tx ∧ V ∈ Tx) ∧ x1 ∈ U) ∧ x2 ∈ V) (U ∩ V = Empty) HUV).
We prove the intermediate claim HUV2: (U ∈ Tx ∧ V ∈ Tx) ∧ x1 ∈ U.
An exact proof term for the current goal is (andEL ((U ∈ Tx ∧ V ∈ Tx) ∧ x1 ∈ U) (x2 ∈ V) HUV1).
We prove the intermediate claim Hx2V: x2 ∈ V.
An exact proof term for the current goal is (andER ((U ∈ Tx ∧ V ∈ Tx) ∧ x1 ∈ U) (x2 ∈ V) HUV1).
We prove the intermediate claim HUV3: U ∈ Tx ∧ V ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx ∧ V ∈ Tx) (x1 ∈ U) HUV2).
We prove the intermediate claim Hx1U: x1 ∈ U.
An exact proof term for the current goal is (andER (U ∈ Tx ∧ V ∈ Tx) (x1 ∈ U) HUV2).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (V ∈ Tx) HUV3).
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (andER (U ∈ Tx) (V ∈ Tx) HUV3).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUinTx).
We prove the intermediate claim HVsubX: V ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V HTx HVinTx).
We prove the intermediate claim HpnotU: p ∉ U.
Assume HpU: p ∈ U.
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (HUsubX p HpU).
We prove the intermediate claim HpEq: p = X.
Use reflexivity.
We prove the intermediate claim HXself: X ∈ X.
rewrite the current goal using HpEq (from right to left).
An exact proof term for the current goal is HpX.
An exact proof term for the current goal is ((In_irref X) HXself).
We prove the intermediate claim HpnotV: p ∉ V.
Assume HpV: p ∈ V.
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (HVsubX p HpV).
We prove the intermediate claim HpEq: p = X.
Use reflexivity.
We prove the intermediate claim HXself: X ∈ X.
rewrite the current goal using HpEq (from right to left).
An exact proof term for the current goal is HpX.
An exact proof term for the current goal is ((In_irref X) HXself).
We prove the intermediate claim HUsubY: U ⊆ Y.
Let z be given.
Assume HzU: z ∈ U.
An exact proof term for the current goal is (binunionI1 X {p} z (HUsubX z HzU)).
We prove the intermediate claim HVsubY: V ⊆ Y.
Let z be given.
Assume HzV: z ∈ V.
An exact proof term for the current goal is (binunionI1 X {p} z (HVsubX z HzV)).
We prove the intermediate claim HUpowY: U ∈ 𝒫 Y.
An exact proof term for the current goal is (PowerI Y U HUsubY).
We prove the intermediate claim HVpowY: V ∈ 𝒫 Y.
An exact proof term for the current goal is (PowerI Y V HVsubY).
We prove the intermediate claim HUinTy: U ∈ Ty.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) U HUpowY (orIL (p ∉ U ∧ U ∈ Tx) (p ∈ U ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U = Y ∖ K) (andI (p ∉ U) (U ∈ Tx) HpnotU HUinTx))).
We prove the intermediate claim HVinTy: V ∈ Ty.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) V HVpowY (orIL (p ∉ V ∧ V ∈ Tx) (p ∈ V ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ V = Y ∖ K) (andI (p ∉ V) (V ∈ Tx) HpnotV HVinTx))).
Apply and5I to the current goal.
An exact proof term for the current goal is HUinTy.
An exact proof term for the current goal is HVinTy.
An exact proof term for the current goal is Hx1U.
An exact proof term for the current goal is Hx2V.
An exact proof term for the current goal is HUVempty.
Assume Hx2p: x2 ∈ {p}.
We prove the intermediate claim Hx2eq: x2 = p.
An exact proof term for the current goal is (SingE p x2 Hx2p).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (locally_compact_topology X Tx Hlc).
Apply (locally_compact_local X Tx x1 Hlc Hx1X) to the current goal.
Let U be given.
Assume HU0.
We prove the intermediate claim HUleft: U ∈ Tx ∧ x1 ∈ U.
An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x1 ∈ U) (compact_space (closure_of X Tx U) (subspace_topology X Tx (closure_of X Tx U))) HU0).
We prove the intermediate claim HKcomp: compact_space (closure_of X Tx U) (subspace_topology X Tx (closure_of X Tx U)).
An exact proof term for the current goal is (andER (U ∈ Tx ∧ x1 ∈ U) (compact_space (closure_of X Tx U) (subspace_topology X Tx (closure_of X Tx U))) HU0).
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (x1 ∈ U) HUleft).
We prove the intermediate claim Hx1U: x1 ∈ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (x1 ∈ U) HUleft).
Set K to be the term closure_of X Tx U.
Set V to be the term Y ∖ K.
We prove the intermediate claim HKsubX: K ⊆ X.
An exact proof term for the current goal is (closure_in_space X Tx U HTx).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUopen).
We prove the intermediate claim HUsubK: U ⊆ K.
An exact proof term for the current goal is (subset_of_closure X Tx U HTx HUsubX).
We prove the intermediate claim HpnotU: p ∉ U.
Assume HpU: p ∈ U.
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (HUsubX p HpU).
We prove the intermediate claim HpEq: p = X.
Use reflexivity.
We prove the intermediate claim HXself: X ∈ X.
rewrite the current goal using HpEq (from right to left).
An exact proof term for the current goal is HpX.
An exact proof term for the current goal is ((In_irref X) HXself).
We prove the intermediate claim HUsubY: U ⊆ Y.
Let z be given.
Assume HzU: z ∈ U.
An exact proof term for the current goal is (binunionI1 X {p} z (HUsubX z HzU)).
We prove the intermediate claim HUpowY: U ∈ 𝒫 Y.
An exact proof term for the current goal is (PowerI Y U HUsubY).
We prove the intermediate claim HUinTy: U ∈ Ty.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 = Y ∖ K0)) U HUpowY (orIL (p ∉ U ∧ U ∈ Tx) (p ∈ U ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U = Y ∖ K0) (andI (p ∉ U) (U ∈ Tx) HpnotU HUopen))).
We prove the intermediate claim HVsubY: V ⊆ Y.
Let z be given.
Assume Hz: z ∈ V.
An exact proof term for the current goal is (setminusE1 Y K z Hz).
We prove the intermediate claim HVpowY: V ∈ 𝒫 Y.
An exact proof term for the current goal is (PowerI Y V HVsubY).
We prove the intermediate claim HpY: p ∈ Y.
An exact proof term for the current goal is (binunionI2 X {p} p (SingI p)).
We prove the intermediate claim HpnotK: p ∉ K.
Assume HpK: p ∈ K.
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (HKsubX p HpK).
We prove the intermediate claim HpEq: p = X.
Use reflexivity.
We prove the intermediate claim HXself: X ∈ X.
rewrite the current goal using HpEq (from right to left).
An exact proof term for the current goal is HpX.
An exact proof term for the current goal is ((In_irref X) HXself).
We prove the intermediate claim HpV: p ∈ V.
An exact proof term for the current goal is (setminusI Y K p HpY HpnotK).
We prove the intermediate claim HVinTy: V ∈ Ty.
Apply (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 = Y ∖ K0)) V HVpowY) to the current goal.
We will prove (p ∉ V ∧ V ∈ Tx) ∨ (p ∈ V ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ V = Y ∖ K0).
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HpV.
We use K to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HKcomp.
An exact proof term for the current goal is HKsubX.
Use reflexivity.
We prove the intermediate claim HUVempty: U ∩ V = Empty.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ U ∩ V.
Apply FalseE to the current goal.
We prove the intermediate claim Hzpair: z ∈ U ∧ z ∈ V.
An exact proof term for the current goal is (binintersectE U V z Hz).
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (andEL (z ∈ U) (z ∈ V) Hzpair).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (andER (z ∈ U) (z ∈ V) Hzpair).
We prove the intermediate claim HzK: z ∈ K.
An exact proof term for the current goal is (HUsubK z HzU).
We prove the intermediate claim HznotK: z ∉ K.
An exact proof term for the current goal is (setminusE2 Y K z HzV).
An exact proof term for the current goal is (HznotK HzK).
An exact proof term for the current goal is (Subq_Empty (U ∩ V)).
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is HUinTy.
An exact proof term for the current goal is HVinTy.
An exact proof term for the current goal is Hx1U.
rewrite the current goal using Hx2eq (from left to right).
An exact proof term for the current goal is HpV.
An exact proof term for the current goal is HUVempty.
Assume Hx1p: x1 ∈ {p}.
We prove the intermediate claim Hx1eq: x1 = p.
An exact proof term for the current goal is (SingE p x1 Hx1p).
Apply (binunionE X {p} x2 Hx2Y (∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty)) to the current goal.
Assume Hx2X: x2 ∈ X.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (locally_compact_topology X Tx Hlc).
Apply (locally_compact_local X Tx x2 Hlc Hx2X) to the current goal.
Let U0 be given.
Assume HU0.
We prove the intermediate claim HUleft: U0 ∈ Tx ∧ x2 ∈ U0.
An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ x2 ∈ U0) (compact_space (closure_of X Tx U0) (subspace_topology X Tx (closure_of X Tx U0))) HU0).
We prove the intermediate claim HKcomp: compact_space (closure_of X Tx U0) (subspace_topology X Tx (closure_of X Tx U0)).
An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ x2 ∈ U0) (compact_space (closure_of X Tx U0) (subspace_topology X Tx (closure_of X Tx U0))) HU0).
We prove the intermediate claim HUopen: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (x2 ∈ U0) HUleft).
We prove the intermediate claim Hx2U: x2 ∈ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (x2 ∈ U0) HUleft).
Set K0 to be the term closure_of X Tx U0.
Set V0 to be the term Y ∖ K0.
We prove the intermediate claim HKsubX: K0 ⊆ X.
An exact proof term for the current goal is (closure_in_space X Tx U0 HTx).
We prove the intermediate claim HUsubX: U0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U0 HTx HUopen).
We prove the intermediate claim HUsubK: U0 ⊆ K0.
An exact proof term for the current goal is (subset_of_closure X Tx U0 HTx HUsubX).
We prove the intermediate claim HpnotU: p ∉ U0.
Assume HpU: p ∈ U0.
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (HUsubX p HpU).
We prove the intermediate claim HpEq: p = X.
Use reflexivity.
We prove the intermediate claim HXself: X ∈ X.
rewrite the current goal using HpEq (from right to left).
An exact proof term for the current goal is HpX.
An exact proof term for the current goal is ((In_irref X) HXself).
We prove the intermediate claim HUsubY: U0 ⊆ Y.
Let z be given.
Assume HzU: z ∈ U0.
An exact proof term for the current goal is (binunionI1 X {p} z (HUsubX z HzU)).
We prove the intermediate claim HUpowY: U0 ∈ 𝒫 Y.
An exact proof term for the current goal is (PowerI Y U0 HUsubY).
We prove the intermediate claim HUinTy: U0 ∈ Ty.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU1 : set ⇒ (p ∉ U1 ∧ U1 ∈ Tx) ∨ (p ∈ U1 ∧ ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U1 = Y ∖ K1)) U0 HUpowY (orIL (p ∉ U0 ∧ U0 ∈ Tx) (p ∈ U0 ∧ ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U0 = Y ∖ K1) (andI (p ∉ U0) (U0 ∈ Tx) HpnotU HUopen))).
We prove the intermediate claim HVsubY: V0 ⊆ Y.
Let z be given.
Assume Hz: z ∈ V0.
An exact proof term for the current goal is (setminusE1 Y K0 z Hz).
We prove the intermediate claim HVpowY: V0 ∈ 𝒫 Y.
An exact proof term for the current goal is (PowerI Y V0 HVsubY).
We prove the intermediate claim HpY: p ∈ Y.
An exact proof term for the current goal is (binunionI2 X {p} p (SingI p)).
We prove the intermediate claim HpnotK: p ∉ K0.
Assume HpK: p ∈ K0.
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (HKsubX p HpK).
We prove the intermediate claim HpEq: p = X.
Use reflexivity.
We prove the intermediate claim HXself: X ∈ X.
rewrite the current goal using HpEq (from right to left).
An exact proof term for the current goal is HpX.
An exact proof term for the current goal is ((In_irref X) HXself).
We prove the intermediate claim HpV: p ∈ V0.
An exact proof term for the current goal is (setminusI Y K0 p HpY HpnotK).
We prove the intermediate claim HVinTy: V0 ∈ Ty.
Apply (SepI (𝒫 Y) (λU1 : set ⇒ (p ∉ U1 ∧ U1 ∈ Tx) ∨ (p ∈ U1 ∧ ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U1 = Y ∖ K1)) V0 HVpowY) to the current goal.
We will prove (p ∉ V0 ∧ V0 ∈ Tx) ∨ (p ∈ V0 ∧ ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ V0 = Y ∖ K1).
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HpV.
We use K0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HKcomp.
An exact proof term for the current goal is HKsubX.
Use reflexivity.
We prove the intermediate claim HUVempty: U0 ∩ V0 = Empty.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ U0 ∩ V0.
Apply FalseE to the current goal.
We prove the intermediate claim Hzpair: z ∈ U0 ∧ z ∈ V0.
An exact proof term for the current goal is (binintersectE U0 V0 z Hz).
We prove the intermediate claim HzU: z ∈ U0.
An exact proof term for the current goal is (andEL (z ∈ U0) (z ∈ V0) Hzpair).
We prove the intermediate claim HzV: z ∈ V0.
An exact proof term for the current goal is (andER (z ∈ U0) (z ∈ V0) Hzpair).
We prove the intermediate claim HzK: z ∈ K0.
An exact proof term for the current goal is (HUsubK z HzU).
We prove the intermediate claim HznotK: z ∉ K0.
An exact proof term for the current goal is (setminusE2 Y K0 z HzV).
An exact proof term for the current goal is (HznotK HzK).
An exact proof term for the current goal is (Subq_Empty (U0 ∩ V0)).
We use V0 to witness the existential quantifier.
We use U0 to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is HVinTy.
An exact proof term for the current goal is HUinTy.
rewrite the current goal using Hx1eq (from left to right).
An exact proof term for the current goal is HpV.
An exact proof term for the current goal is Hx2U.
rewrite the current goal using (binintersect_com V0 U0) (from left to right).
An exact proof term for the current goal is HUVempty.
Assume Hx2p: x2 ∈ {p}.
We prove the intermediate claim Hx1p': x1 = p.
An exact proof term for the current goal is (SingE p x1 Hx1p).
We prove the intermediate claim Hx2p': x2 = p.
An exact proof term for the current goal is (SingE p x2 Hx2p).
Apply FalseE to the current goal.
Apply Hneq to the current goal.
rewrite the current goal using Hx1p' (from left to right).
rewrite the current goal using Hx2p' (from left to right).
Use reflexivity.
We prove the intermediate claim HcompY: compact_space Y Ty.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (Hausdorff_space_topology Y Ty HHausY).
We will prove compact_space Y Ty.
We will prove topology_on Y Ty ∧ ∀Fam : set, open_cover_of Y Ty Fam → has_finite_subcover Y Ty Fam.
Apply andI to the current goal.
An exact proof term for the current goal is HTy.
Let Fam be given.
Assume HFam: open_cover_of Y Ty Fam.
We will prove has_finite_subcover Y Ty Fam.
We prove the intermediate claim HYcov: Y ⊆ ⋃ Fam.
An exact proof term for the current goal is (open_cover_of_covers Y Ty Fam HFam).
We prove the intermediate claim HpY: p ∈ Y.
An exact proof term for the current goal is (binunionI2 X {p} p (SingI p)).
We prove the intermediate claim HpUnion: p ∈ ⋃ Fam.
An exact proof term for the current goal is (HYcov p HpY).
Apply (UnionE_impred Fam p HpUnion) to the current goal.
Let U0 be given.
Assume HpU0: p ∈ U0.
Assume HU0Fam: U0 ∈ Fam.
We prove the intermediate claim HU0Ty: U0 ∈ Ty.
An exact proof term for the current goal is (open_cover_of_members_open Y Ty Fam U0 HFam HU0Fam).
We prove the intermediate claim HU0prop: (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 = Y ∖ K0).
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU1 : set ⇒ (p ∉ U1 ∧ U1 ∈ Tx) ∨ (p ∈ U1 ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U1 = Y ∖ K0)) U0 HU0Ty).
Apply HU0prop to the current goal.
Assume Hbad: p ∉ U0 ∧ U0 ∈ Tx.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((andEL (p ∉ U0) (U0 ∈ Tx) Hbad) HpU0).
Assume Hgood: p ∈ U0 ∧ ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 = Y ∖ K0.
We prove the intermediate claim HexK0: ∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 = Y ∖ K0.
An exact proof term for the current goal is (andER (p ∈ U0) (∃K0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 = Y ∖ K0) Hgood).
Apply HexK0 to the current goal.
Let K0 be given.
Assume HK0pkg.
We prove the intermediate claim HK0left: compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X.
An exact proof term for the current goal is (andEL (compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X) (U0 = Y ∖ K0) HK0pkg).
We prove the intermediate claim HK0comp: compact_space K0 (subspace_topology X Tx K0).
An exact proof term for the current goal is (andEL (compact_space K0 (subspace_topology X Tx K0)) (K0 ⊆ X) HK0left).
We prove the intermediate claim HK0subX: K0 ⊆ X.
An exact proof term for the current goal is (andER (compact_space K0 (subspace_topology X Tx K0)) (K0 ⊆ X) HK0left).
We prove the intermediate claim HU0eq: U0 = Y ∖ K0.
An exact proof term for the current goal is (andER (compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X) (U0 = Y ∖ K0) HK0pkg).
We prove the intermediate claim HTxX: topology_on X Tx.
An exact proof term for the current goal is (locally_compact_topology X Tx Hlc).
Set FamX to be the term {V ∈ Tx|∃U : set, U ∈ Fam ∧ V = U ∩ X}.
We prove the intermediate claim HFamXsub: FamX ⊆ Tx.
Let V be given.
Assume HV: V ∈ FamX.
An exact proof term for the current goal is (SepE1 Tx (λV0 : set ⇒ ∃U : set, U ∈ Fam ∧ V0 = U ∩ X) V HV).
We prove the intermediate claim HK0covFamX: K0 ⊆ ⋃ FamX.
Let x be given.
Assume HxK0: x ∈ K0.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HK0subX x HxK0).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binunionI1 X {p} x HxX).
We prove the intermediate claim HxUnionFam: x ∈ ⋃ Fam.
An exact proof term for the current goal is (HYcov x HxY).
Apply (UnionE_impred Fam x HxUnionFam) to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HUinFam: U ∈ Fam.
We prove the intermediate claim HUinTy: U ∈ Ty.
An exact proof term for the current goal is (open_cover_of_members_open Y Ty Fam U HFam HUinFam).
We prove the intermediate claim HUprop: (p ∉ U ∧ U ∈ Tx) ∨ (p ∈ U ∧ ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U = Y ∖ K1).
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU1 : set ⇒ (p ∉ U1 ∧ U1 ∈ Tx) ∨ (p ∈ U1 ∧ ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U1 = Y ∖ K1)) U HUinTy).
Set V to be the term U ∩ X.
We prove the intermediate claim HVTx: V ∈ Tx.
Apply HUprop to the current goal.
Assume Hcase: p ∉ U ∧ U ∈ Tx.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andER (p ∉ U) (U ∈ Tx) Hcase).
We prove the intermediate claim HUs: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTxX HUinTx).
rewrite the current goal using (binintersect_Subq_eq_1 U X HUs) (from left to right).
An exact proof term for the current goal is HUinTx.
Assume Hcase: p ∈ U ∧ ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U = Y ∖ K1.
We prove the intermediate claim HexK1: ∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U = Y ∖ K1.
An exact proof term for the current goal is (andER (p ∈ U) (∃K1 : set, compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X ∧ U = Y ∖ K1) Hcase).
Apply HexK1 to the current goal.
Let K1 be given.
Assume HK1pkg.
We prove the intermediate claim HK1left: compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X.
An exact proof term for the current goal is (andEL (compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X) (U = Y ∖ K1) HK1pkg).
We prove the intermediate claim HK1comp: compact_space K1 (subspace_topology X Tx K1).
An exact proof term for the current goal is (andEL (compact_space K1 (subspace_topology X Tx K1)) (K1 ⊆ X) HK1left).
We prove the intermediate claim HK1subX: K1 ⊆ X.
An exact proof term for the current goal is (andER (compact_space K1 (subspace_topology X Tx K1)) (K1 ⊆ X) HK1left).
We prove the intermediate claim HUeq1: U = Y ∖ K1.
An exact proof term for the current goal is (andER (compact_space K1 (subspace_topology X Tx K1) ∧ K1 ⊆ X) (U = Y ∖ K1) HK1pkg).
We prove the intermediate claim HK1closed: closed_in X Tx K1.
An exact proof term for the current goal is (Hausdorff_compact_sets_closed X Tx K1 HH HK1subX HK1comp).
We prove the intermediate claim Hop: open_in X Tx (X ∖ K1).
An exact proof term for the current goal is (open_of_closed_complement X Tx K1 HK1closed).
We prove the intermediate claim HXK1: (X ∖ K1) ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ K1) Hop).
rewrite the current goal using HUeq1 (from left to right).
We prove the intermediate claim HeqV: (Y ∖ K1) ∩ X = X ∖ K1.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ (Y ∖ K1) ∩ X.
We prove the intermediate claim HyYK1: y ∈ Y ∖ K1.
An exact proof term for the current goal is (binintersectE1 (Y ∖ K1) X y Hy).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (binintersectE2 (Y ∖ K1) X y Hy).
We prove the intermediate claim HynotK1: y ∉ K1.
An exact proof term for the current goal is (setminusE2 Y K1 y HyYK1).
An exact proof term for the current goal is (setminusI X K1 y HyX HynotK1).
Let y be given.
Assume Hy: y ∈ X ∖ K1.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (setminusE1 X K1 y Hy).
We prove the intermediate claim HynotK1: y ∉ K1.
An exact proof term for the current goal is (setminusE2 X K1 y Hy).
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (binunionI1 X {p} y HyX).
We prove the intermediate claim HyYK1: y ∈ Y ∖ K1.
An exact proof term for the current goal is (setminusI Y K1 y HyY HynotK1).
An exact proof term for the current goal is (binintersectI (Y ∖ K1) X y HyYK1 HyX).
rewrite the current goal using HeqV (from left to right).
An exact proof term for the current goal is HXK1.
We prove the intermediate claim HVinFamX: V ∈ FamX.
Apply (SepI Tx (λV0 : set ⇒ ∃U0 : set, U0 ∈ Fam ∧ V0 = U0 ∩ X) V) to the current goal.
An exact proof term for the current goal is HVTx.
We will prove ∃U0 : set, U0 ∈ Fam ∧ V = U0 ∩ X.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUinFam.
Use reflexivity.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectI U X x HxU HxX).
An exact proof term for the current goal is (UnionI FamX x V HxV HVinFamX).
We prove the intermediate claim HK0equiv: (compact_space K0 (subspace_topology X Tx K0) ↔ ∀Fam0 : set, (Fam0 ⊆ Tx ∧ K0 ⊆ ⋃ Fam0) → has_finite_subcover K0 Tx Fam0).
An exact proof term for the current goal is (compact_subspace_via_ambient_covers X Tx K0 HTxX HK0subX).
We prove the intermediate claim HK0amb: ∀Fam0 : set, (Fam0 ⊆ Tx ∧ K0 ⊆ ⋃ Fam0) → has_finite_subcover K0 Tx Fam0.
An exact proof term for the current goal is (iffEL (compact_space K0 (subspace_topology X Tx K0)) (∀Fam0 : set, (Fam0 ⊆ Tx ∧ K0 ⊆ ⋃ Fam0) → has_finite_subcover K0 Tx Fam0) HK0equiv HK0comp).
We prove the intermediate claim HfinX: has_finite_subcover K0 Tx FamX.
An exact proof term for the current goal is (HK0amb FamX (andI (FamX ⊆ Tx) (K0 ⊆ ⋃ FamX) HFamXsub HK0covFamX)).
Apply HfinX to the current goal.
Let Gx be given.
Assume HGx.
We prove the intermediate claim HGxleft: Gx ⊆ FamX ∧ finite Gx.
An exact proof term for the current goal is (andEL (Gx ⊆ FamX ∧ finite Gx) (K0 ⊆ ⋃ Gx) HGx).
We prove the intermediate claim HGxsub: Gx ⊆ FamX.
An exact proof term for the current goal is (andEL (Gx ⊆ FamX) (finite Gx) HGxleft).
We prove the intermediate claim HGxfin: finite Gx.
An exact proof term for the current goal is (andER (Gx ⊆ FamX) (finite Gx) HGxleft).
We prove the intermediate claim HK0covGx: K0 ⊆ ⋃ Gx.
An exact proof term for the current goal is (andER (Gx ⊆ FamX ∧ finite Gx) (K0 ⊆ ⋃ Gx) HGx).
Set pickU to be the term λV : set ⇒ Eps_i (λU : set ⇒ U ∈ Fam ∧ V = U ∩ X).
Set Gpre to be the term {pickU V|V ∈ Gx}.
We prove the intermediate claim HGpreFin: finite Gpre.
An exact proof term for the current goal is (Repl_finite (λV : set ⇒ pickU V) Gx HGxfin).
We prove the intermediate claim HGpreSub: Gpre ⊆ Fam.
Let U be given.
Assume HU: U ∈ Gpre.
We prove the intermediate claim HexV: ∃V : set, V ∈ Gx ∧ U = pickU V.
An exact proof term for the current goal is (ReplE Gx (λV0 : set ⇒ pickU V0) U HU).
Apply HexV to the current goal.
Let V be given.
Assume HVand.
We prove the intermediate claim HVinGx: V ∈ Gx.
An exact proof term for the current goal is (andEL (V ∈ Gx) (U = pickU V) HVand).
We prove the intermediate claim HUeqp: U = pickU V.
An exact proof term for the current goal is (andER (V ∈ Gx) (U = pickU V) HVand).
We prove the intermediate claim HVinFamX: V ∈ FamX.
An exact proof term for the current goal is (HGxsub V HVinGx).
We prove the intermediate claim HexU: ∃U0 : set, U0 ∈ Fam ∧ V = U0 ∩ X.
An exact proof term for the current goal is (SepE2 Tx (λV0 : set ⇒ ∃U0 : set, U0 ∈ Fam ∧ V0 = U0 ∩ X) V HVinFamX).
We prove the intermediate claim Hpick: (pickU V) ∈ Fam ∧ V = (pickU V) ∩ X.
Apply HexU to the current goal.
Let U0 be given.
Assume HU0and.
An exact proof term for the current goal is (Eps_i_ax (λU1 : set ⇒ U1 ∈ Fam ∧ V = U1 ∩ X) U0 HU0and).
rewrite the current goal using HUeqp (from left to right).
An exact proof term for the current goal is (andEL ((pickU V) ∈ Fam) (V = (pickU V) ∩ X) Hpick).
We prove the intermediate claim HK0covGpre: K0 ⊆ ⋃ Gpre.
Let x be given.
Assume HxK0: x ∈ K0.
We prove the intermediate claim HxUnion: x ∈ ⋃ Gx.
An exact proof term for the current goal is (HK0covGx x HxK0).
Apply (UnionE_impred Gx x HxUnion) to the current goal.
Let V be given.
Assume HxV: x ∈ V.
Assume HVinGx: V ∈ Gx.
We prove the intermediate claim HVinFamX: V ∈ FamX.
An exact proof term for the current goal is (HGxsub V HVinGx).
We prove the intermediate claim HexU: ∃U0 : set, U0 ∈ Fam ∧ V = U0 ∩ X.
An exact proof term for the current goal is (SepE2 Tx (λV0 : set ⇒ ∃U0 : set, U0 ∈ Fam ∧ V0 = U0 ∩ X) V HVinFamX).
We prove the intermediate claim Hpick: (pickU V) ∈ Fam ∧ V = (pickU V) ∩ X.
Apply HexU to the current goal.
Let U0 be given.
Assume HU0and.
An exact proof term for the current goal is (Eps_i_ax (λU1 : set ⇒ U1 ∈ Fam ∧ V = U1 ∩ X) U0 HU0and).
We prove the intermediate claim HxPick: x ∈ pickU V.
We prove the intermediate claim HxV': x ∈ (pickU V) ∩ X.
We prove the intermediate claim HeqV: V = (pickU V) ∩ X.
An exact proof term for the current goal is (andER ((pickU V) ∈ Fam) (V = (pickU V) ∩ X) Hpick).
rewrite the current goal using HeqV (from right to left).
An exact proof term for the current goal is HxV.
An exact proof term for the current goal is (binintersectE1 (pickU V) X x HxV').
We prove the intermediate claim HpickInGpre: pickU V ∈ Gpre.
An exact proof term for the current goal is (ReplI Gx (λV0 : set ⇒ pickU V0) V HVinGx).
An exact proof term for the current goal is (UnionI Gpre x (pickU V) HxPick HpickInGpre).
Set G to be the term Gpre ∪ {U0}.
Apply (has_finite_subcoverI Y Ty Fam G) to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let U be given.
Assume HU: U ∈ G.
Apply (binunionE Gpre {U0} U HU (U ∈ Fam)) to the current goal.
Assume HUpre: U ∈ Gpre.
An exact proof term for the current goal is (HGpreSub U HUpre).
Assume HUsing: U ∈ {U0}.
We prove the intermediate claim Heq: U = U0.
An exact proof term for the current goal is (SingE U0 U HUsing).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HU0Fam.
An exact proof term for the current goal is (binunion_finite Gpre HGpreFin {U0} (Sing_finite U0)).
Let y be given.
Assume HyY: y ∈ Y.
Apply (binunionE X {p} y HyY (y ∈ ⋃ G)) to the current goal.
Assume HyX: y ∈ X.
Apply (xm (y ∈ U0)) to the current goal.
Assume HyU0: y ∈ U0.
An exact proof term for the current goal is (UnionI G y U0 HyU0 (binunionI2 Gpre {U0} U0 (SingI U0))).
Assume HyNotU0: ¬ (y ∈ U0).
We prove the intermediate claim HyK0: y ∈ K0.
Apply (xm (y ∈ K0)) to the current goal.
Assume HyK0.
An exact proof term for the current goal is HyK0.
Assume HyNotK0: ¬ (y ∈ K0).
We prove the intermediate claim HyU0': y ∈ U0.
rewrite the current goal using HU0eq (from left to right).
An exact proof term for the current goal is (setminusI Y K0 y HyY HyNotK0).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HyNotU0 HyU0').
We prove the intermediate claim HyUnionPre: y ∈ ⋃ Gpre.
An exact proof term for the current goal is (HK0covGpre y HyK0).
Apply (UnionE_impred Gpre y HyUnionPre) to the current goal.
Let U be given.
Assume HyU: y ∈ U.
Assume HUpre: U ∈ Gpre.
An exact proof term for the current goal is (UnionI G y U HyU (binunionI1 Gpre {U0} U HUpre)).
Assume Hyp: y ∈ {p}.
We prove the intermediate claim Heq: y = p.
An exact proof term for the current goal is (SingE p y Hyp).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (UnionI G p U0 HpU0 (binunionI2 Gpre {U0} U0 (SingI U0))).
We prove the intermediate claim HXsubY: X ⊆ Y.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (binunionI1 X {p} x HxX).
We prove the intermediate claim HexPoint: ∃p0 : set, p0 ∈ Y ∧ ¬ p0 ∈ X ∧ subspace_topology Y Ty X = Tx ∧ (∀y : set, y ∈ Y → y ∈ X ∨ y = p0).
We use p to witness the existential quantifier.
Apply andI to the current goal.
We will prove (p ∈ Y ∧ ¬ p ∈ X) ∧ subspace_topology Y Ty X = Tx.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI2 X {p} p (SingI p)).
We prove the intermediate claim HpEq: p = X.
Use reflexivity.
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is (In_irref X).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (locally_compact_topology X Tx Hlc).
Apply set_ext to the current goal.
Let W be given.
Assume HW: W ∈ subspace_topology Y Ty X.
We will prove W ∈ Tx.
We prove the intermediate claim Hex: ∃V ∈ Ty, W = V ∩ X.
An exact proof term for the current goal is (subspace_topologyE Y Ty X W HW).
Apply Hex to the current goal.
Let V be given.
Assume HVpair.
We prove the intermediate claim HV: V ∈ Ty.
An exact proof term for the current goal is (andEL (V ∈ Ty) (W = V ∩ X) HVpair).
We prove the intermediate claim HWeq: W = V ∩ X.
An exact proof term for the current goal is (andER (V ∈ Ty) (W = V ∩ X) HVpair).
We prove the intermediate claim HVprop: (p ∉ V ∧ V ∈ Tx) ∨ (p ∈ V ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ V = Y ∖ K).
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) V HV).
Apply HVprop to the current goal.
Assume Hcase: p ∉ V ∧ V ∈ Tx.
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (andER (p ∉ V) (V ∈ Tx) Hcase).
We prove the intermediate claim HVsubX: V ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V HTx HVinTx).
We prove the intermediate claim HVeq: V ∩ X = V.
An exact proof term for the current goal is (binintersect_Subq_eq_1 V X HVsubX).
We prove the intermediate claim HWeqV: W = V.
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is HVeq.
rewrite the current goal using HWeqV (from left to right).
An exact proof term for the current goal is HVinTx.
Assume Hcase: p ∈ V ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ V = Y ∖ K.
We prove the intermediate claim HexK: ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ V = Y ∖ K.
An exact proof term for the current goal is (andER (p ∈ V) (∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ V = Y ∖ K) Hcase).
Apply HexK to the current goal.
Let K be given.
Assume HKpkg.
We prove the intermediate claim HKleft: compact_space K (subspace_topology X Tx K) ∧ K ⊆ X.
An exact proof term for the current goal is (andEL (compact_space K (subspace_topology X Tx K) ∧ K ⊆ X) (V = Y ∖ K) HKpkg).
We prove the intermediate claim HKcomp: compact_space K (subspace_topology X Tx K).
An exact proof term for the current goal is (andEL (compact_space K (subspace_topology X Tx K)) (K ⊆ X) HKleft).
We prove the intermediate claim HKsubX: K ⊆ X.
An exact proof term for the current goal is (andER (compact_space K (subspace_topology X Tx K)) (K ⊆ X) HKleft).
We prove the intermediate claim HVe: V = Y ∖ K.
An exact proof term for the current goal is (andER (compact_space K (subspace_topology X Tx K) ∧ K ⊆ X) (V = Y ∖ K) HKpkg).
We prove the intermediate claim HWdef: W = (Y ∖ K) ∩ X.
rewrite the current goal using HWeq (from left to right).
rewrite the current goal using HVe (from left to right).
Use reflexivity.
We prove the intermediate claim HeqWXK: (Y ∖ K) ∩ X = X ∖ K.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (Y ∖ K) ∩ X.
We will prove x ∈ X ∖ K.
We prove the intermediate claim Hpair: x ∈ (Y ∖ K) ∧ x ∈ X.
An exact proof term for the current goal is (binintersectE (Y ∖ K) X x Hx).
We prove the intermediate claim HxYK: x ∈ Y ∖ K.
An exact proof term for the current goal is (andEL (x ∈ Y ∖ K) (x ∈ X) Hpair).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andER (x ∈ Y ∖ K) (x ∈ X) Hpair).
We prove the intermediate claim HxnotK: x ∉ K.
An exact proof term for the current goal is (setminusE2 Y K x HxYK).
An exact proof term for the current goal is (setminusI X K x HxX HxnotK).
Let x be given.
Assume Hx: x ∈ X ∖ K.
We will prove x ∈ (Y ∖ K) ∩ X.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X K x Hx).
We prove the intermediate claim HxnotK: x ∉ K.
An exact proof term for the current goal is (setminusE2 X K x Hx).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binunionI1 X {p} x HxX).
We prove the intermediate claim HxYK: x ∈ Y ∖ K.
An exact proof term for the current goal is (setminusI Y K x HxY HxnotK).
An exact proof term for the current goal is (binintersectI (Y ∖ K) X x HxYK HxX).
We prove the intermediate claim HWis: W = X ∖ K.
rewrite the current goal using HWdef (from left to right).
An exact proof term for the current goal is HeqWXK.
rewrite the current goal using HWis (from left to right).
We prove the intermediate claim HKclosed: closed_in X Tx K.
An exact proof term for the current goal is (Hausdorff_compact_sets_closed X Tx K HH HKsubX HKcomp).
We prove the intermediate claim HKpkg2: K ⊆ X ∧ ∃U : set, U ∈ Tx ∧ K = X ∖ U.
An exact proof term for the current goal is (closed_in_package X Tx K HKclosed).
We prove the intermediate claim HexU: ∃U : set, U ∈ Tx ∧ K = X ∖ U.
An exact proof term for the current goal is (andER (K ⊆ X) (∃U : set, U ∈ Tx ∧ K = X ∖ U) HKpkg2).
Apply HexU to the current goal.
Let U be given.
Assume HUpkg.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (K = X ∖ U) HUpkg).
We prove the intermediate claim HKeq: K = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (K = X ∖ U) HUpkg).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUinTx).
We prove the intermediate claim HeqXminusK: X ∖ K = U.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X ∖ K.
We will prove x ∈ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X K x Hx).
We prove the intermediate claim HxnotK: x ∉ K.
An exact proof term for the current goal is (setminusE2 X K x Hx).
We prove the intermediate claim HxnotXU: x ∉ X ∖ U.
rewrite the current goal using HKeq (from right to left).
An exact proof term for the current goal is HxnotK.
Apply (xm (x ∈ U)) to the current goal.
Assume HxU: x ∈ U.
An exact proof term for the current goal is HxU.
Assume HxnotU: ¬ (x ∈ U).
We prove the intermediate claim HxXU: x ∈ X ∖ U.
An exact proof term for the current goal is (setminusI X U x HxX HxnotU).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotXU HxXU).
Let x be given.
Assume Hx: x ∈ U.
We will prove x ∈ X ∖ K.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsubX x Hx).
We prove the intermediate claim HxnotK: x ∉ K.
Assume HxK: x ∈ K.
We prove the intermediate claim HxXU: x ∈ X ∖ U.
rewrite the current goal using HKeq (from right to left).
An exact proof term for the current goal is HxK.
We prove the intermediate claim HxnotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 X U x HxXU).
An exact proof term for the current goal is (HxnotU Hx).
An exact proof term for the current goal is (setminusI X K x HxX HxnotK).
rewrite the current goal using HeqXminusK (from left to right).
An exact proof term for the current goal is HUinTx.
Let W be given.
Assume HW: W ∈ Tx.
We will prove W ∈ subspace_topology Y Ty X.
We prove the intermediate claim HWsubX: W ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx W HTx HW).
We prove the intermediate claim HWsubY: W ⊆ Y.
Let x be given.
Assume HxW: x ∈ W.
An exact proof term for the current goal is (binunionI1 X {p} x (HWsubX x HxW)).
We prove the intermediate claim HWpowY: W ∈ 𝒫 Y.
An exact proof term for the current goal is (PowerI Y W HWsubY).
We prove the intermediate claim HpnotW: p ∉ W.
Assume HpW: p ∈ W.
We prove the intermediate claim HpX: p ∈ X.
An exact proof term for the current goal is (HWsubX p HpW).
We prove the intermediate claim HpEq: p = X.
Use reflexivity.
We prove the intermediate claim HXself: X ∈ X.
rewrite the current goal using HpEq (from right to left).
An exact proof term for the current goal is HpX.
An exact proof term for the current goal is ((In_irref X) HXself).
We prove the intermediate claim HWTy: W ∈ Ty.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ (p ∉ U0 ∧ U0 ∈ Tx) ∨ (p ∈ U0 ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U0 = Y ∖ K)) W HWpowY (orIL (p ∉ W ∧ W ∈ Tx) (p ∈ W ∧ ∃K : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ W = Y ∖ K) (andI (p ∉ W) (W ∈ Tx) HpnotW HW))).
We prove the intermediate claim HWpowX: W ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X W HWsubX).
We prove the intermediate claim HeqW: W = W ∩ X.
rewrite the current goal using (binintersect_Subq_eq_1 W X HWsubX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hex: ∃V ∈ Ty, W = V ∩ X.
We use W to witness the existential quantifier.
An exact proof term for the current goal is (andI (W ∈ Ty) (W = W ∩ X) HWTy HeqW).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∃V ∈ Ty, U0 = V ∩ X) W HWpowX Hex).
Let y be given.
Assume Hy: y ∈ Y.
Apply (binunionE X {p} y Hy) to the current goal.
Assume HyX: y ∈ X.
An exact proof term for the current goal is (orIL (y ∈ X) (y = p) HyX).
Assume Hyp: y ∈ {p}.
We prove the intermediate claim Heq: y = p.
An exact proof term for the current goal is (SingE p y Hyp).
An exact proof term for the current goal is (orIR (y ∈ X) (y = p) Heq).
We will prove one_point_compactification X Tx Y Ty.
An exact proof term for the current goal is (andI ((compact_space Y Ty ∧ Hausdorff_space Y Ty) ∧ X ⊆ Y) (∃p0 : set, p0 ∈ Y ∧ ¬ p0 ∈ X ∧ subspace_topology Y Ty X = Tx ∧ (∀y : set, y ∈ Y → y ∈ X ∨ y = p0)) (andI (compact_space Y Ty ∧ Hausdorff_space Y Ty) (X ⊆ Y) (andI (compact_space Y Ty) (Hausdorff_space Y Ty) HcompY HHausY) HXsubY) HexPoint).
∎