Let X be given.
We will prove completely_regular_space X (discrete_topology X).
We prove the intermediate claim HTx: topology_on X (discrete_topology X).
An exact proof term for the current goal is (discrete_topology_on X).
We will prove topology_on X (discrete_topology X) ∧ (one_point_sets_closed X (discrete_topology X) ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X (discrete_topology X) F → x ∉ F → ∃f : set, continuous_map X (discrete_topology X) 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.
An exact proof term for the current goal is (andEL (one_point_sets_closed X (discrete_topology X)) (∀A B : set, closed_in X (discrete_topology X) A → closed_in X (discrete_topology X) B → A ∩ B = Empty → ∃U V : set, U ∈ discrete_topology X ∧ V ∈ discrete_topology X ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) (discrete_normal_space X)).
Let x be given.
Assume HxX: x ∈ X.
Let F be given.
Assume HFcl: closed_in X (discrete_topology X) F.
Assume HxnotF: x ∉ F.
We will prove ∃f : set, continuous_map X (discrete_topology X) R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1.
We prove the intermediate claim HFsubX: F ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (discrete_topology X) F HFcl).
Set A0 to be the term X ∖ F.
We prove the intermediate claim HA0def: A0 = X ∖ F.
Use reflexivity.
Set f to be the term (const_fun A0 0) ∪ (const_fun F 1).
We use f to witness the existential quantifier.
We prove the intermediate claim HRtop: 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 H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim H1R: 1 ∈ R.
An exact proof term for the current goal is real_1.
We prove the intermediate claim Happ0: ∀z : set, z ∈ X → z ∉ F → apply_fun f z = 0.
Let z be given.
Assume HzX: z ∈ X.
Assume HznotF: z ∉ F.
We will prove apply_fun f z = 0.
We prove the intermediate claim HzA0: z ∈ A0.
rewrite the current goal using HA0def (from left to right).
An exact proof term for the current goal is (setminusI X F z HzX HznotF).
We prove the intermediate claim Hpair0: (z,0) ∈ f.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is (ReplI A0 (λa0 : set ⇒ (a0,0)) z HzA0).
We prove the intermediate claim Hzgraph: (z,apply_fun f z) ∈ f.
An exact proof term for the current goal is (Eps_i_ax (λy : set ⇒ (z,y) ∈ f) 0 Hpair0).
Apply (binunionE' (const_fun A0 0) (const_fun F 1) (z,apply_fun f z) (apply_fun f z = 0)) to the current goal.
Assume Hleft: (z,apply_fun f z) ∈ const_fun A0 0.
An exact proof term for the current goal is (const_fun_pair_second A0 0 z (apply_fun f z) Hleft).
Assume Hright: (z,apply_fun f z) ∈ const_fun F 1.
We prove the intermediate claim HzF: z ∈ F.
An exact proof term for the current goal is (const_fun_pair_first F 1 z (apply_fun f z) Hright).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HznotF HzF).
An exact proof term for the current goal is Hzgraph.
We prove the intermediate claim Happ1: ∀z : set, z ∈ X → z ∈ F → apply_fun f z = 1.
Let z be given.
Assume HzX: z ∈ X.
Assume HzF: z ∈ F.
We will prove apply_fun f z = 1.
We prove the intermediate claim Hpair1: (z,1) ∈ f.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is (ReplI F (λa0 : set ⇒ (a0,1)) z HzF).
We prove the intermediate claim Hzgraph: (z,apply_fun f z) ∈ f.
An exact proof term for the current goal is (Eps_i_ax (λy : set ⇒ (z,y) ∈ f) 1 Hpair1).
Apply (binunionE' (const_fun A0 0) (const_fun F 1) (z,apply_fun f z) (apply_fun f z = 1)) to the current goal.
Assume Hleft: (z,apply_fun f z) ∈ const_fun A0 0.
We prove the intermediate claim HzA0: z ∈ A0.
An exact proof term for the current goal is (const_fun_pair_first A0 0 z (apply_fun f z) Hleft).
We prove the intermediate claim HznotF: z ∉ F.
We prove the intermediate claim HzXF: z ∈ X ∖ F.
rewrite the current goal using HA0def (from right to left).
An exact proof term for the current goal is HzA0.
An exact proof term for the current goal is (setminusE2 X F z HzXF).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HznotF HzF).
Assume Hright: (z,apply_fun f z) ∈ const_fun F 1.
An exact proof term for the current goal is (const_fun_pair_second F 1 z (apply_fun f z) Hright).
An exact proof term for the current goal is Hzgraph.
We prove the intermediate claim Hfun: function_on f X R.
Let z be given.
Assume HzX: z ∈ X.
We will prove apply_fun f z ∈ R.
Apply (xm (z ∈ F)) to the current goal.
Assume HzF: z ∈ F.
We prove the intermediate claim Hz1: apply_fun f z = 1.
An exact proof term for the current goal is (Happ1 z HzX HzF).
rewrite the current goal using Hz1 (from left to right).
An exact proof term for the current goal is H1R.
Assume HznotF: z ∉ F.
We prove the intermediate claim Hz0: apply_fun f z = 0.
An exact proof term for the current goal is (Happ0 z HzX HznotF).
rewrite the current goal using Hz0 (from left to right).
An exact proof term for the current goal is H0R.
We prove the intermediate claim Hcont: continuous_map X (discrete_topology X) R R_standard_topology f.
An exact proof term for the current goal is (continuous_from_discrete X R R_standard_topology f HRtop Hfun).
We prove the intermediate claim Hfx0: apply_fun f x = 0.
An exact proof term for the current goal is (Happ0 x HxX HxnotF).
We prove the intermediate claim HfF1: ∀y : set, y ∈ F → apply_fun f y = 1.
Let y be given.
Assume HyF: y ∈ F.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HFsubX y HyF).
An exact proof term for the current goal is (Happ1 y HyX HyF).
Apply andI to the current goal.
We will prove continuous_map X (discrete_topology X) 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 Hcont.
An exact proof term for the current goal is Hfx0.
An exact proof term for the current goal is HfF1.
∎