Let X and Tx be given.
Assume Hnorm: normal_space X Tx.
We will prove completely_regular_space X Tx.
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 (normal_space_topology_on X Tx Hnorm).
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) Hnorm).
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.
We prove the intermediate claim Hone: one_point_sets_closed X Tx.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) Hnorm).
We prove the intermediate claim Hxcl: closed_in X Tx {x}.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x0 : set, x0 ∈ X → closed_in X Tx {x0}) Hone x HxX).
We prove the intermediate claim Hdisj: {x} ∩ F = Empty.
Apply set_ext to the current goal.
Let u be given.
Assume Hu: u ∈ {x} ∩ F.
We will prove u ∈ Empty.
We prove the intermediate claim Hux: u ∈ {x}.
An exact proof term for the current goal is (binintersectE1 {x} F u Hu).
We prove the intermediate claim HuEq: u = x.
An exact proof term for the current goal is (SingE x u Hux).
We prove the intermediate claim HuF: u ∈ F.
An exact proof term for the current goal is (binintersectE2 {x} F u Hu).
We prove the intermediate claim HxF: x ∈ F.
rewrite the current goal using HuEq (from right to left).
An exact proof term for the current goal is HuF.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotF HxF).
Let u be given.
Assume Hu: u ∈ Empty.
An exact proof term for the current goal is (EmptyE u Hu (u ∈ {x} ∩ F)).
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 Hex: ∃f : set, continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀u : set, u ∈ {x} → apply_fun f u = 0) ∧ (∀u : set, u ∈ F → apply_fun f u = 1).
An exact proof term for the current goal is (Urysohn_lemma X Tx {x} F 0 1 H0le1 Hnorm Hxcl HFcl Hdisj).
Apply Hex to the current goal.
Let f be given.
Assume Hfpack.
We use f to witness the existential quantifier.
We prove the intermediate claim Hpair1: continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀u : set, u ∈ {x} → apply_fun f u = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀u : set, u ∈ {x} → apply_fun f u = 0)) (∀u : set, u ∈ F → apply_fun f u = 1) Hfpack).
We prove the intermediate claim HcontI: continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f.
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f) (∀u : set, u ∈ {x} → apply_fun f u = 0) Hpair1).
We prove the intermediate claim HAx: ∀u : set, u ∈ {x} → apply_fun f u = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f) (∀u : set, u ∈ {x} → apply_fun f u = 0) Hpair1).
We prove the intermediate claim Hfx0: apply_fun f x = 0.
An exact proof term for the current goal is (HAx x (SingI x)).
We prove the intermediate claim HfF1: ∀y : set, y ∈ F → apply_fun f y = 1.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀u : set, u ∈ {x} → apply_fun f u = 0)) (∀u : set, u ∈ F → apply_fun f u = 1) Hfpack).
We prove the intermediate claim HISubR: 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 HTIeq: closed_interval_topology 0 1 = subspace_topology R R_standard_topology (closed_interval 0 1).
Use reflexivity.
We prove the intermediate claim HcontR: continuous_map X Tx R R_standard_topology f.
An exact proof term for the current goal is (continuous_map_range_expand X Tx (closed_interval 0 1) (closed_interval_topology 0 1) R R_standard_topology f HcontI HISubR R_standard_topology_is_topology HTIeq).
Apply andI to the current goal.
We will prove continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0.
Apply andI to the current goal.
An exact proof term for the current goal is HcontR.
An exact proof term for the current goal is Hfx0.
An exact proof term for the current goal is HfF1.
∎