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 prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (Hausdorff_space_topology X Tx HH).
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.
Set U0 to be the term X ∖ F.
We prove the intermediate claim HU0open: open_in X Tx U0.
An exact proof term for the current goal is (open_of_closed_complement X Tx F HFcl).
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U0 HU0open).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (setminusI X F x HxX HxnotF).
Apply (locally_compact_local X Tx x Hlc HxX) to the current goal.
Let U1 be given.
Assume HU1: U1 ∈ Tx ∧ x ∈ U1 ∧ compact_space (closure_of X Tx U1) (subspace_topology X Tx (closure_of X Tx U1)).
Set K to be the term closure_of X Tx U1.
Set Tk to be the term subspace_topology X Tx K.
Set Y to be the term F ∩ K.
We prove the intermediate claim HU1a: (U1 ∈ Tx ∧ x ∈ U1) ∧ compact_space K Tk.
An exact proof term for the current goal is HU1.
We prove the intermediate claim HU1b: U1 ∈ Tx ∧ x ∈ U1.
An exact proof term for the current goal is (andEL (U1 ∈ Tx ∧ x ∈ U1) (compact_space K Tk) HU1a).
We prove the intermediate claim HcompK: compact_space K Tk.
An exact proof term for the current goal is (andER (U1 ∈ Tx ∧ x ∈ U1) (compact_space K Tk) HU1a).
We prove the intermediate claim HU1Tx: U1 ∈ Tx.
An exact proof term for the current goal is (andEL (U1 ∈ Tx) (x ∈ U1) HU1b).
We prove the intermediate claim HxU1: x ∈ U1.
An exact proof term for the current goal is (andER (U1 ∈ Tx) (x ∈ U1) HU1b).
We prove the intermediate claim HU1subX: U1 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U1 HTx HU1Tx).
We prove the intermediate claim HKsubX: K ⊆ X.
An exact proof term for the current goal is (closure_in_space X Tx U1 HTx).
We prove the intermediate claim HYsubK: Y ⊆ K.
Let z be given.
Assume HzY: z ∈ Y.
An exact proof term for the current goal is (binintersectE2 F K z HzY).
We prove the intermediate claim HYsubX: Y ⊆ X.
Let z be given.
Assume HzY: z ∈ Y.
Apply HKsubX to the current goal.
An exact proof term for the current goal is (HYsubK z HzY).
We prove the intermediate claim HKclosed: closed_in X Tx K.
An exact proof term for the current goal is (closure_is_closed X Tx U1 HTx HU1subX).
We prove the intermediate claim HYclosedK: closed_in K Tk Y.
Apply (iffER (closed_in K Tk Y) (∃C : set, closed_in X Tx C ∧ Y = C ∩ K) (closed_in_subspace_iff_intersection X Tx K Y 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 HcompY_sub: compact_space Y (subspace_topology K Tk Y).
An exact proof term for the current goal is (closed_subspace_compact K Tk Y HcompK HYclosedK).
We prove the intermediate claim Hsubtrans: subspace_topology K Tk Y = subspace_topology X Tx Y.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx K Y HTx HKsubX HYsubK).
We prove the intermediate claim HcompY: compact_space Y (subspace_topology X Tx Y).
rewrite the current goal using Hsubtrans (from right to left).
An exact proof term for the current goal is HcompY_sub.
We prove the intermediate claim HxnotY: x ∉ Y.
Assume HxY: x ∈ Y.
We prove the intermediate claim HxF: x ∈ F.
An exact proof term for the current goal is (binintersectE1 F K x HxY).
Apply HxnotF to the current goal.
An exact proof term for the current goal is HxF.
Apply (Hausdorff_separate_point_compact_set X Tx Y x HH HYsubX HcompY HxX HxnotY) to the current goal.
Let U3 be given.
Assume HU3: ∃V3 : set, U3 ∈ Tx ∧ V3 ∈ Tx ∧ x ∈ U3 ∧ Y ⊆ V3 ∧ U3 ∩ V3 = Empty.
Apply HU3 to the current goal.
Let V3 be given.
Assume HUV3: U3 ∈ Tx ∧ V3 ∈ Tx ∧ x ∈ U3 ∧ Y ⊆ V3 ∧ U3 ∩ V3 = Empty.
Set U to be the term U3 ∩ U1.
Set V to be the term V3 ∪ (X ∖ K).
We prove the intermediate claim H1234: ((U3 ∈ Tx ∧ V3 ∈ Tx) ∧ x ∈ U3) ∧ Y ⊆ V3.
An exact proof term for the current goal is (andEL (((U3 ∈ Tx ∧ V3 ∈ Tx) ∧ x ∈ U3) ∧ Y ⊆ V3) (U3 ∩ V3 = Empty) HUV3).
We prove the intermediate claim Hdisj: U3 ∩ V3 = Empty.
An exact proof term for the current goal is (andER (((U3 ∈ Tx ∧ V3 ∈ Tx) ∧ x ∈ U3) ∧ Y ⊆ V3) (U3 ∩ V3 = Empty) HUV3).
We prove the intermediate claim H123: (U3 ∈ Tx ∧ V3 ∈ Tx) ∧ x ∈ U3.
An exact proof term for the current goal is (andEL ((U3 ∈ Tx ∧ V3 ∈ Tx) ∧ x ∈ U3) (Y ⊆ V3) H1234).
We prove the intermediate claim HYsubV3: Y ⊆ V3.
An exact proof term for the current goal is (andER ((U3 ∈ Tx ∧ V3 ∈ Tx) ∧ x ∈ U3) (Y ⊆ V3) H1234).
We prove the intermediate claim H12: U3 ∈ Tx ∧ V3 ∈ Tx.
An exact proof term for the current goal is (andEL (U3 ∈ Tx ∧ V3 ∈ Tx) (x ∈ U3) H123).
We prove the intermediate claim HxU3: x ∈ U3.
An exact proof term for the current goal is (andER (U3 ∈ Tx ∧ V3 ∈ Tx) (x ∈ U3) H123).
We prove the intermediate claim HU3Tx: U3 ∈ Tx.
An exact proof term for the current goal is (andEL (U3 ∈ Tx) (V3 ∈ Tx) H12).
We prove the intermediate claim HV3Tx: V3 ∈ Tx.
An exact proof term for the current goal is (andER (U3 ∈ Tx) (V3 ∈ Tx) H12).
We prove the intermediate claim HXKopen: open_in X Tx (X ∖ K).
An exact proof term for the current goal is (open_of_closed_complement X Tx K HKclosed).
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) HXKopen).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx U3 U1 HTx HU3Tx HU1Tx).
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (topology_binunion_closed X Tx V3 (X ∖ K) HTx HV3Tx HXKTx).
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 HUinTx.
An exact proof term for the current goal is HVinTx.
We will prove x ∈ U.
An exact proof term for the current goal is (binintersectI U3 U1 x HxU3 HxU1).
We will prove F ⊆ V.
We prove the intermediate claim HFsubX: F ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx F HFcl).
Let y be given.
Assume HyF: y ∈ F.
Apply (xm (y ∈ K)) to the current goal.
Assume HyK: y ∈ K.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (binintersectI F K y HyF HyK).
We prove the intermediate claim HyV3: y ∈ V3.
An exact proof term for the current goal is (HYsubV3 y HyY).
An exact proof term for the current goal is (binunionI1 V3 (X ∖ K) y HyV3).
Assume HnotK: ¬ (y ∈ K).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HFsubX 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 HnotK).
An exact proof term for the current goal is (binunionI2 V3 (X ∖ K) y HyXK).
We will prove U ∩ V = Empty.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ U ∩ V.
We will prove z ∈ Empty.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE1 U V z Hz).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (binintersectE2 U V z Hz).
We prove the intermediate claim HzU3: z ∈ U3.
An exact proof term for the current goal is (binintersectE1 U3 U1 z HzU).
We prove the intermediate claim HzU1: z ∈ U1.
An exact proof term for the current goal is (binintersectE2 U3 U1 z HzU).
Apply (binunionE V3 (X ∖ K) z HzV) to the current goal.
Assume HzV3: z ∈ V3.
We prove the intermediate claim HzUV: z ∈ U3 ∩ V3.
An exact proof term for the current goal is (binintersectI U3 V3 z HzU3 HzV3).
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HzUV.
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).
We prove the intermediate claim HU1subK: U1 ⊆ K.
An exact proof term for the current goal is (closure_contains_set X Tx U1 HTx HU1subX).
We prove the intermediate claim HzK: z ∈ K.
An exact proof term for the current goal is (HU1subK z HzU1).
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 Hz: z ∈ Empty.
We will prove z ∈ U ∩ V.
An exact proof term for the current goal is (EmptyE z Hz (z ∈ U ∩ V)).
∎