Let X and Tx be given.
Assume Hlc: locally_compact X Tx.
Assume HH: Hausdorff_space X Tx.
We will prove completely_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 topology_on X Tx ∧ (one_point_sets_closed X Tx ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Apply andI to the current goal.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → closed_in X Tx {x}.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (Hausdorff_singletons_closed X Tx x HH HxX).
Let x be given.
Assume HxX: x ∈ X.
Let F be given.
Assume HFcl: closed_in X Tx F.
Assume HxnotF: x ∉ F.
We will prove ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1.
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).
We prove the intermediate claim Hreg: regular_space X Tx.
An exact proof term for the current goal is (ex32_3_locally_compact_Hausdorff_regular X Tx Hlc HH).
We prove the intermediate claim HexV0: ∃V0 : set, V0 ∈ Tx ∧ x ∈ V0 ∧ closure_of X Tx V0 ⊆ U0.
An exact proof term for the current goal is (regular_space_shrink_neighborhood X Tx x U0 Hreg HxX HU0Tx HxU0).
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ Tx ∧ x ∈ V0 ∧ closure_of X Tx V0 ⊆ U0.
We prove the intermediate claim HV0pair: (V0 ∈ Tx ∧ x ∈ V0) ∧ closure_of X Tx V0 ⊆ U0.
An exact proof term for the current goal is HV0.
We prove the intermediate claim HV0Tx_x: V0 ∈ Tx ∧ x ∈ V0.
An exact proof term for the current goal is (andEL (V0 ∈ Tx ∧ x ∈ V0) (closure_of X Tx V0 ⊆ U0) HV0pair).
We prove the intermediate claim HclV0subU0: closure_of X Tx V0 ⊆ U0.
An exact proof term for the current goal is (andER (V0 ∈ Tx ∧ x ∈ V0) (closure_of X Tx V0 ⊆ U0) HV0pair).
We prove the intermediate claim HV0Tx: V0 ∈ Tx.
An exact proof term for the current goal is (andEL (V0 ∈ Tx) (x ∈ V0) HV0Tx_x).
We prove the intermediate claim HxV0: x ∈ V0.
An exact proof term for the current goal is (andER (V0 ∈ Tx) (x ∈ V0) HV0Tx_x).
We prove the intermediate claim HexU1: ∃U1 : set, U1 ∈ Tx ∧ x ∈ U1 ∧ compact_space (closure_of X Tx U1) (subspace_topology X Tx (closure_of X Tx U1)).
An exact proof term for the current goal is (locally_compact_local X Tx x Hlc HxX).
Apply HexU1 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)).
We prove the intermediate claim HU1pair: (U1 ∈ Tx ∧ x ∈ U1) ∧ compact_space (closure_of X Tx U1) (subspace_topology X Tx (closure_of X Tx U1)).
An exact proof term for the current goal is HU1.
We prove the intermediate claim HU1Tx_x: U1 ∈ Tx ∧ x ∈ U1.
An exact proof term for the current goal is (andEL (U1 ∈ Tx ∧ x ∈ U1) (compact_space (closure_of X Tx U1) (subspace_topology X Tx (closure_of X Tx U1))) HU1pair).
We prove the intermediate claim HcompK1: compact_space (closure_of X Tx U1) (subspace_topology X Tx (closure_of X Tx U1)).
An exact proof term for the current goal is (andER (U1 ∈ Tx ∧ x ∈ U1) (compact_space (closure_of X Tx U1) (subspace_topology X Tx (closure_of X Tx U1))) HU1pair).
We prove the intermediate claim HU1Tx: U1 ∈ Tx.
An exact proof term for the current goal is (andEL (U1 ∈ Tx) (x ∈ U1) HU1Tx_x).
We prove the intermediate claim HxU1: x ∈ U1.
An exact proof term for the current goal is (andER (U1 ∈ Tx) (x ∈ U1) HU1Tx_x).
Set W to be the term V0 ∩ U1.
We prove the intermediate claim HWTx: W ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx V0 U1 HTx HV0Tx HU1Tx).
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (binintersectI V0 U1 x HxV0 HxU1).
We prove the intermediate claim HWsubV0: W ⊆ V0.
An exact proof term for the current goal is (binintersect_Subq_1 V0 U1).
We prove the intermediate claim HWsubU0: W ⊆ U0.
Let z be given.
Assume HzW: z ∈ W.
An exact proof term for the current goal is (HclV0subU0 z ((subset_of_closure X Tx V0 HTx (topology_elem_subset X Tx V0 HTx HV0Tx)) z (HWsubV0 z HzW))).
Set K1 to be the term closure_of X Tx U1.
Set TK1 to be the term subspace_topology X Tx K1.
Set K to be the term closure_of X Tx W.
Set TK to be the term subspace_topology X Tx K.
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 HV0subX: V0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V0 HTx HV0Tx).
We prove the intermediate claim HWsubX: W ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx W HTx HWTx).
We prove the intermediate claim HKsubX: K ⊆ X.
An exact proof term for the current goal is (closure_in_space X Tx W HTx).
We prove the intermediate claim HK1subX: K1 ⊆ X.
An exact proof term for the current goal is (closure_in_space X Tx U1 HTx).
We prove the intermediate claim HWsubU1: W ⊆ U1.
An exact proof term for the current goal is (binintersect_Subq_2 V0 U1).
We prove the intermediate claim HclWsubK1: K ⊆ K1.
An exact proof term for the current goal is (closure_monotone X Tx W U1 HTx HWsubU1 HU1subX).
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 W HTx HWsubX).
We prove the intermediate claim HKeq: K = K ∩ K1.
Apply set_ext to the current goal.
Let z be given.
Assume HzK: z ∈ K.
Apply (binintersectI K K1 z) to the current goal.
An exact proof term for the current goal is HzK.
An exact proof term for the current goal is (HclWsubK1 z HzK).
Let z be given.
Assume Hz: z ∈ K ∩ K1.
An exact proof term for the current goal is (binintersectE1 K K1 z Hz).
We prove the intermediate claim HKclosed_in_K1: closed_in K1 TK1 K.
Apply (iffER (closed_in K1 TK1 K) (∃C : set, closed_in X Tx C ∧ K = C ∩ K1) (closed_in_subspace_iff_intersection X Tx K1 K HTx HK1subX)) to the current goal.
We use K to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HKclosed.
An exact proof term for the current goal is HKeq.
We prove the intermediate claim HcompK: compact_space K (subspace_topology X Tx K).
We prove the intermediate claim HcompK_sub: compact_space K (subspace_topology K1 TK1 K).
An exact proof term for the current goal is (closed_subspace_compact K1 TK1 K HcompK1 HKclosed_in_K1).
We prove the intermediate claim Htrans: subspace_topology K1 TK1 K = subspace_topology X Tx K.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx K1 K HTx HK1subX HclWsubK1).
rewrite the current goal using Htrans (from right to left).
An exact proof term for the current goal is HcompK_sub.
We prove the intermediate claim HHK1: Hausdorff_space K1 TK1.
An exact proof term for the current goal is (ex17_12_subspace_Hausdorff X Tx K1 HH HK1subX).
We prove the intermediate claim HHK: Hausdorff_space K (subspace_topology X Tx K).
An exact proof term for the current goal is (ex17_12_subspace_Hausdorff X Tx K HH HKsubX).
We prove the intermediate claim HnormK: normal_space K (subspace_topology X Tx K).
An exact proof term for the current goal is (compact_Hausdorff_normal K (subspace_topology X Tx K) HcompK HHK).
We prove the intermediate claim HxK: x ∈ K.
An exact proof term for the current goal is (subset_of_closure X Tx W HTx HWsubX x (binintersectI V0 U1 x HxV0 HxU1)).
We prove the intermediate claim HWsubK: W ⊆ K.
An exact proof term for the current goal is (subset_of_closure X Tx W HTx HWsubX).
We prove the intermediate claim HWsubK': W ⊆ K.
An exact proof term for the current goal is HWsubK.
We prove the intermediate claim HWopenK: open_in K (subspace_topology X Tx K) W.
Apply (iffER (open_in K (subspace_topology X Tx K) W) (∃V ∈ Tx, W = V ∩ K) (open_in_subspace_iff X Tx K W HTx HKsubX HWsubK')) to the current goal.
We use W to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HWTx.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ W.
An exact proof term for the current goal is (binintersectI W K z Hz (HWsubK z Hz)).
Let z be given.
Assume Hz: z ∈ W ∩ K.
An exact proof term for the current goal is (binintersectE1 W K z Hz).
We prove the intermediate claim HWcomp_closed: closed_in K (subspace_topology X Tx K) (K ∖ W).
An exact proof term for the current goal is (closed_of_open_complement K (subspace_topology X Tx K) W (subspace_topology_is_topology X Tx K HTx HKsubX) (open_in_elem K (subspace_topology X Tx K) W HWopenK)).
We prove the intermediate claim HsingClosed: closed_in K (subspace_topology X Tx K) {x}.
An exact proof term for the current goal is (Hausdorff_singletons_closed K (subspace_topology X Tx K) x HHK HxK).
We prove the intermediate claim HxnotKW: x ∉ (K ∖ W).
Assume HxKW: x ∈ K ∖ W.
We prove the intermediate claim HxnotW: x ∉ W.
An exact proof term for the current goal is (andER (x ∈ K) (x ∉ W) (setminusE K W x HxKW)).
An exact proof term for the current goal is (HxnotW HxW).
We prove the intermediate claim Hdisj: {x} ∩ (K ∖ W) = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ {x} ∩ (K ∖ W).
We will prove z ∈ Empty.
We prove the intermediate claim Hzx: z ∈ {x}.
An exact proof term for the current goal is (binintersectE1 {x} (K ∖ W) z Hz).
We prove the intermediate claim Hzeq: z = x.
An exact proof term for the current goal is (SingE x z Hzx).
We prove the intermediate claim HzKW: z ∈ (K ∖ W).
An exact proof term for the current goal is (binintersectE2 {x} (K ∖ W) z Hz).
We prove the intermediate claim HxKW: x ∈ (K ∖ W).
rewrite the current goal using Hzeq (from right to left).
An exact proof term for the current goal is HzKW.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotKW HxKW).
We prove the intermediate claim H0le1: Rle 0 1.
An exact proof term for the current goal is (Rlt_implies_Rle 0 1 Rlt_0_1).
We prove the intermediate claim HexfI: ∃fI : set, continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI ∧ (∀z : set, z ∈ {x} → apply_fun fI z = 0) ∧ (∀z : set, z ∈ (K ∖ W) → apply_fun fI z = 1).
An exact proof term for the current goal is (Urysohn_lemma K (subspace_topology X Tx K) {x} (K ∖ W) 0 1 H0le1 HnormK HsingClosed HWcomp_closed Hdisj).
Apply HexfI to the current goal.
Let fI be given.
Assume HfI: continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI ∧ (∀z : set, z ∈ {x} → apply_fun fI z = 0) ∧ (∀z : set, z ∈ (K ∖ W) → apply_fun fI z = 1).
We prove the intermediate claim HfIcont: continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI.
We prove the intermediate claim HfIpair: (continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI ∧ (∀z : set, z ∈ {x} → apply_fun fI z = 0)) ∧ (∀z : set, z ∈ (K ∖ W) → apply_fun fI z = 1).
An exact proof term for the current goal is HfI.
We prove the intermediate claim HfI12: continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI ∧ (∀z : set, z ∈ {x} → apply_fun fI z = 0).
An exact proof term for the current goal is (andEL (continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI ∧ (∀z : set, z ∈ {x} → apply_fun fI z = 0)) (∀z : set, z ∈ (K ∖ W) → apply_fun fI z = 1) HfIpair).
An exact proof term for the current goal is (andEL (continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI) (∀z : set, z ∈ {x} → apply_fun fI z = 0) HfI12).
We prove the intermediate claim HfI0: ∀z : set, z ∈ {x} → apply_fun fI z = 0.
We prove the intermediate claim HfIpair: (continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI ∧ (∀z : set, z ∈ {x} → apply_fun fI z = 0)) ∧ (∀z : set, z ∈ (K ∖ W) → apply_fun fI z = 1).
An exact proof term for the current goal is HfI.
We prove the intermediate claim HfI12: continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI ∧ (∀z : set, z ∈ {x} → apply_fun fI z = 0).
An exact proof term for the current goal is (andEL (continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI ∧ (∀z : set, z ∈ {x} → apply_fun fI z = 0)) (∀z : set, z ∈ (K ∖ W) → apply_fun fI z = 1) HfIpair).
An exact proof term for the current goal is (andER (continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI) (∀z : set, z ∈ {x} → apply_fun fI z = 0) HfI12).
We prove the intermediate claim HfKW1: ∀z : set, z ∈ (K ∖ W) → apply_fun fI z = 1.
We prove the intermediate claim HfIpair: (continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI ∧ (∀z : set, z ∈ {x} → apply_fun fI z = 0)) ∧ (∀z : set, z ∈ (K ∖ W) → apply_fun fI z = 1).
An exact proof term for the current goal is HfI.
An exact proof term for the current goal is (andER (continuous_map K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) fI ∧ (∀z : set, z ∈ {x} → apply_fun fI z = 0)) (∀z : set, z ∈ (K ∖ W) → apply_fun fI z = 1) HfIpair).
We prove the intermediate claim Hfx0: apply_fun fI x = 0.
An exact proof term for the current goal is (HfI0 x (SingI x)).
We prove the intermediate claim HCI_sub_R: closed_interval 0 1 ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R 0 1).
We prove the intermediate claim HTstd: topology_on R R_standard_topology.
An exact proof term for the current goal is (R_standard_topology_is_topology).
We prove the intermediate claim HTIeq: closed_interval_topology 0 1 = subspace_topology R R_standard_topology (closed_interval 0 1).
Use reflexivity.
We prove the intermediate claim HfR: continuous_map K (subspace_topology X Tx K) R R_standard_topology fI.
An exact proof term for the current goal is (continuous_map_range_expand K (subspace_topology X Tx K) (closed_interval 0 1) (closed_interval_topology 0 1) R R_standard_topology fI HfIcont HCI_sub_R HTstd HTIeq).
Set B to be the term X ∖ W.
We prove the intermediate claim HBsubX: B ⊆ X.
Apply setminus_Subq to the current goal.
We prove the intermediate claim HBcl: closed_in X Tx B.
An exact proof term for the current goal is (closed_of_open_complement X Tx W HTx HWTx).
We prove the intermediate claim HABeq: K ∪ B = X.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ K ∪ B.
Apply (binunionE K B z Hz) to the current goal.
Assume HzK: z ∈ K.
An exact proof term for the current goal is (HKsubX z HzK).
Assume HzB: z ∈ B.
An exact proof term for the current goal is (setminusE1 X W z HzB).
Let z be given.
Assume HzX: z ∈ X.
Apply (xm (z ∈ W)) to the current goal.
Assume HzW: z ∈ W.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is (subset_of_closure X Tx W HTx HWsubX z HzW).
Assume HznotW: z ∉ W.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is (setminusI X W z HzX HznotW).
Set g1 to be the term const_fun B 1.
We prove the intermediate claim HTB: topology_on B (subspace_topology X Tx B).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx B HTx HBsubX).
We prove the intermediate claim Hg1: continuous_map B (subspace_topology X Tx B) R R_standard_topology g1.
An exact proof term for the current goal is (const_fun_continuous B (subspace_topology X Tx B) R R_standard_topology 1 HTB R_standard_topology_is_topology_local real_1).
We prove the intermediate claim Hagree: ∀z : set, z ∈ (K ∩ B) → apply_fun fI z = apply_fun g1 z.
Let z be given.
Assume HzKB: z ∈ K ∩ B.
We prove the intermediate claim HzK: z ∈ K.
An exact proof term for the current goal is (binintersectE1 K B z HzKB).
We prove the intermediate claim HzB: z ∈ B.
An exact proof term for the current goal is (binintersectE2 K B z HzKB).
We prove the intermediate claim HzKW: z ∈ (K ∖ W).
We prove the intermediate claim HznotW: z ∉ W.
An exact proof term for the current goal is (andER (z ∈ X) (z ∉ W) (setminusE X W z HzB)).
An exact proof term for the current goal is (setminusI K W z HzK HznotW).
rewrite the current goal using (const_fun_apply B 1 z HzB) (from left to right).
rewrite the current goal using (HfKW1 z HzKW) (from left to right).
Use reflexivity.
Apply (pasting_lemma X K B R Tx R_standard_topology fI g1 HTx HKclosed HBcl HABeq HfR Hg1 Hagree) to the current goal.
Let f be given.
Assume Hf: continuous_map X Tx R R_standard_topology f ∧ ((∀z : set, z ∈ K → apply_fun f z = apply_fun fI z) ∧ (∀z : set, z ∈ B → apply_fun f z = apply_fun g1 z)).
We use f to witness the existential quantifier.
We will prove continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1.
We prove the intermediate claim Hcont: continuous_map X Tx R R_standard_topology f.
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology f) ((∀z : set, z ∈ K → apply_fun f z = apply_fun fI z) ∧ (∀z : set, z ∈ B → apply_fun f z = apply_fun g1 z)) Hf).
We prove the intermediate claim HfK: ∀z : set, z ∈ K → apply_fun f z = apply_fun fI z.
An exact proof term for the current goal is (andEL (∀z : set, z ∈ K → apply_fun f z = apply_fun fI z) (∀z : set, z ∈ B → apply_fun f z = apply_fun g1 z) (andER (continuous_map X Tx R R_standard_topology f) ((∀z : set, z ∈ K → apply_fun f z = apply_fun fI z) ∧ (∀z : set, z ∈ B → apply_fun f z = apply_fun g1 z)) Hf)).
We prove the intermediate claim HfB: ∀z : set, z ∈ B → apply_fun f z = apply_fun g1 z.
An exact proof term for the current goal is (andER (∀z : set, z ∈ K → apply_fun f z = apply_fun fI z) (∀z : set, z ∈ B → apply_fun f z = apply_fun g1 z) (andER (continuous_map X Tx R R_standard_topology f) ((∀z : set, z ∈ K → apply_fun f z = apply_fun fI z) ∧ (∀z : set, z ∈ B → apply_fun f z = apply_fun g1 z)) Hf)).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hcont.
We prove the intermediate claim Hfx: apply_fun f x = apply_fun fI x.
An exact proof term for the current goal is (HfK x HxK).
rewrite the current goal using Hfx (from left to right).
An exact proof term for the current goal is Hfx0.
Let y be given.
Assume HyF: y ∈ F.
We will prove apply_fun f y = 1.
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 HyB: y ∈ B.
Apply (setminusI X W y HyX) to the current goal.
Assume HyW: y ∈ W.
We prove the intermediate claim HyU0: y ∈ U0.
An exact proof term for the current goal is (HWsubU0 y HyW).
We prove the intermediate claim HyNotF: y ∉ F.
An exact proof term for the current goal is (andER (y ∈ X) (y ∉ F) (setminusE X F y HyU0)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HyNotF HyF).
rewrite the current goal using (HfB y HyB) (from left to right).
rewrite the current goal using (const_fun_apply B 1 y HyB) (from left to right).
Use reflexivity.
∎