Let X and Tx be given.
Assume Hlc: locally_compact X Tx.
Assume HH: Hausdorff_space X Tx.
We will prove regular_space X Tx.
We will prove one_point_sets_closed X Tx ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is (Hausdorff_one_point_sets_closed X Tx HH).
Let x be given.
Assume HxX: x ∈ X.
Let F be given.
Assume HFcl: closed_in X Tx F.
Assume HxnotF: x ∉ F.
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 prove the intermediate claim HexU0: ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ 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 (locally_compact_local X Tx x Hlc HxX).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0pack.
We prove the intermediate claim HU0and: U0 ∈ Tx ∧ x ∈ U0.
An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ x ∈ U0) (compact_space (closure_of X Tx U0) (subspace_topology X Tx (closure_of X Tx U0))) HU0pack).
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (x ∈ U0) HU0and).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (x ∈ U0) HU0and).
We prove the intermediate claim HcompK: 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 ∧ x ∈ U0) (compact_space (closure_of X Tx U0) (subspace_topology X Tx (closure_of X Tx U0))) HU0pack).
Set K to be the term closure_of X Tx U0.
Set Tk to be the term subspace_topology X Tx K.
We prove the intermediate claim HKsubX: K ⊆ X.
An exact proof term for the current goal is (closure_in_space X Tx U0 HTx).
We prove the intermediate claim HKclosed: closed_in X Tx K.
An exact proof term for the current goal is (andER (closure_of X Tx (closure_of X Tx U0) = closure_of X Tx U0) (closed_in X Tx (closure_of X Tx U0)) (closure_idempotent_and_closed X Tx U0 HTx)).
Set C to be the term F ∩ K.
We prove the intermediate claim HCsubK: C ⊆ K.
An exact proof term for the current goal is (binintersect_Subq_2 F K).
We prove the intermediate claim HCsubX: C ⊆ X.
An exact proof term for the current goal is (Subq_tra C K X HCsubK HKsubX).
We prove the intermediate claim HCclosed_in_K: closed_in K Tk C.
Apply (iffER (closed_in K (subspace_topology X Tx K) C) (∃D : set, closed_in X Tx D ∧ C = D ∩ K) (closed_in_subspace_iff_intersection X Tx K C HTx HKsubX)) to the current goal.
We use F to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HFcl.
Use reflexivity.
We prove the intermediate claim HcompC_K: compact_space C (subspace_topology K Tk C).
An exact proof term for the current goal is (closed_subspace_compact K Tk C HcompK HCclosed_in_K).
We prove the intermediate claim HsubCK: C ⊆ K.
An exact proof term for the current goal is HCsubK.
We prove the intermediate claim HeqTopC: subspace_topology K Tk C = subspace_topology X Tx C.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx K C HTx HKsubX HsubCK).
We prove the intermediate claim HcompC: compact_space C (subspace_topology X Tx C).
rewrite the current goal using HeqTopC (from right to left).
An exact proof term for the current goal is HcompC_K.
We prove the intermediate claim HxnotC: x ∉ C.
Assume HxC: x ∈ C.
We prove the intermediate claim HxF: x ∈ F.
An exact proof term for the current goal is (binintersectE1 F K x HxC).
An exact proof term for the current goal is (HxnotF HxF).
We prove the intermediate claim Hsep: ∃U1 V1 : set, U1 ∈ Tx ∧ V1 ∈ Tx ∧ x ∈ U1 ∧ C ⊆ V1 ∧ U1 ∩ V1 = Empty.
An exact proof term for the current goal is (Hausdorff_separate_point_compact_set X Tx C x HH HCsubX HcompC HxX HxnotC).
Apply Hsep to the current goal.
Let U1 be given.
Assume HexV1.
Apply HexV1 to the current goal.
Let V1 be given.
Assume HU1V1pack.
We prove the intermediate claim Hleft4: (((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ x ∈ U1) ∧ C ⊆ V1).
An exact proof term for the current goal is (andEL ((((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ x ∈ U1) ∧ C ⊆ V1)) (U1 ∩ V1 = Empty) HU1V1pack).
We prove the intermediate claim HU1V1Empty: U1 ∩ V1 = Empty.
An exact proof term for the current goal is (andER ((((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ x ∈ U1) ∧ C ⊆ V1)) (U1 ∩ V1 = Empty) HU1V1pack).
We prove the intermediate claim Hleft3: (U1 ∈ Tx ∧ V1 ∈ Tx) ∧ x ∈ U1.
An exact proof term for the current goal is (andEL ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ x ∈ U1) (C ⊆ V1) Hleft4).
We prove the intermediate claim HCV1: C ⊆ V1.
An exact proof term for the current goal is (andER ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ x ∈ U1) (C ⊆ V1) Hleft4).
We prove the intermediate claim HU1V1ab: U1 ∈ Tx ∧ V1 ∈ Tx.
An exact proof term for the current goal is (andEL (U1 ∈ Tx ∧ V1 ∈ Tx) (x ∈ U1) Hleft3).
We prove the intermediate claim HxU1: x ∈ U1.
An exact proof term for the current goal is (andER (U1 ∈ Tx ∧ V1 ∈ Tx) (x ∈ U1) Hleft3).
We prove the intermediate claim HU1Tx: U1 ∈ Tx.
An exact proof term for the current goal is (andEL (U1 ∈ Tx) (V1 ∈ Tx) HU1V1ab).
We prove the intermediate claim HV1Tx: V1 ∈ Tx.
An exact proof term for the current goal is (andER (U1 ∈ Tx) (V1 ∈ Tx) HU1V1ab).
Set U to be the term U1 ∩ U0.
Set V to be the term V1 ∪ (X ∖ K).
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx U1 U0 HTx HU1Tx HU0Tx).
We prove the intermediate claim HKU0sub: U0 ⊆ K.
We prove the intermediate claim HU0subX: U0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U0 HTx HU0Tx).
An exact proof term for the current goal is (subset_of_closure X Tx U0 HTx HU0subX).
We prove the intermediate claim HxU: x ∈ U.
Apply (binintersectI U1 U0 x) to the current goal.
An exact proof term for the current goal is HxU1.
An exact proof term for the current goal is HxU0.
We prove the intermediate claim HXKTx: (X ∖ K) ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ K) (open_of_closed_complement X Tx K HKclosed)).
We prove the intermediate claim HVopen: V ∈ Tx.
An exact proof term for the current goal is (topology_binunion_closed X Tx V1 (X ∖ K) HTx HV1Tx HXKTx).
We prove the intermediate claim HFsubV: F ⊆ V.
Let y be given.
Assume HyF: y ∈ F.
We will prove y ∈ V.
Apply (xm (y ∈ K)) to the current goal.
Assume HyK: y ∈ K.
We prove the intermediate claim HyC: y ∈ C.
Apply (binintersectI F K y) to the current goal.
An exact proof term for the current goal is HyF.
An exact proof term for the current goal is HyK.
We prove the intermediate claim HyV1: y ∈ V1.
An exact proof term for the current goal is (HCV1 y HyC).
An exact proof term for the current goal is (binunionI1 V1 (X ∖ K) y HyV1).
Assume HynK: y ∉ K.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is ((closed_in_subset X Tx F HFcl) y HyF).
We prove the intermediate claim HyXK: y ∈ X ∖ K.
An exact proof term for the current goal is (setminusI X K y HyX HynK).
An exact proof term for the current goal is (binunionI2 V1 (X ∖ K) y HyXK).
We prove the intermediate claim HUcapV: U ∩ V = Empty.
Apply set_ext to the current goal.
Let z be given.
Assume HzUV: z ∈ U ∩ V.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE1 U V z HzUV).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (binintersectE2 U V z HzUV).
We prove the intermediate claim HzU1: z ∈ U1.
An exact proof term for the current goal is (binintersectE1 U1 U0 z HzU).
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (binintersectE2 U1 U0 z HzU).
We prove the intermediate claim HzK: z ∈ K.
An exact proof term for the current goal is (HKU0sub z HzU0).
We prove the intermediate claim HzVor: z ∈ V1 ∨ z ∈ (X ∖ K).
An exact proof term for the current goal is (binunionE V1 (X ∖ K) z HzV).
Apply HzVor to the current goal.
Assume HzV1: z ∈ V1.
We prove the intermediate claim HzU1V1: z ∈ U1 ∩ V1.
Apply (binintersectI U1 V1 z) to the current goal.
An exact proof term for the current goal is HzU1.
An exact proof term for the current goal is HzV1.
We prove the intermediate claim HzEmpty: z ∈ Empty.
rewrite the current goal using HU1V1Empty (from right to left).
An exact proof term for the current goal is HzU1V1.
An exact proof term for the current goal is HzEmpty.
Assume HzXK: z ∈ X ∖ K.
We prove the intermediate claim HznotK: z ∉ K.
An exact proof term for the current goal is (setminusE2 X K z HzXK).
Apply FalseE to the current goal.
We will prove False.
An exact proof term for the current goal is (HznotK HzK).
Let z be given.
Assume HzE: z ∈ Empty.
Apply FalseE to the current goal.
We will prove False.
An exact proof term for the current goal is (EmptyE z HzE).
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
We will prove U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUopen.
An exact proof term for the current goal is HVopen.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HFsubV.
An exact proof term for the current goal is HUcapV.
∎