Let X, Tx, A and V be given.
Assume Hnorm: normal_space X Tx.
Assume HAcl: closed_in X Tx A.
Assume HVopen: V ∈ Tx.
Assume HAsubV: A ⊆ V.
We will prove ∃f : set, continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ A → apply_fun f x = 1) ∧ (∀x : set, x ∈ (X ∖ V) → apply_fun f x = 0) ∧ (∀x : set, x ∈ X → apply_fun f x ∈ unit_interval).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
We prove the intermediate claim HVcl: closed_in X Tx (X ∖ V).
An exact proof term for the current goal is (closed_of_open_complement X Tx V HTx HVopen).
We prove the intermediate claim Hdisj: (X ∖ V) ∩ A = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (X ∖ V) ∩ A.
We will prove x ∈ Empty.
We prove the intermediate claim HxOut: x ∈ (X ∖ V).
An exact proof term for the current goal is (binintersectE1 (X ∖ V) A x Hx).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE2 (X ∖ V) A x Hx).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (HAsubV x HxA).
We prove the intermediate claim HxNotV: x ∉ V.
An exact proof term for the current goal is (setminusE2 X V x HxOut).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxNotV HxV).
Let x be given.
Assume HxE: x ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
We prove the intermediate claim H01: 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 HexU: ∃f0 : set, continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f0 ∧ (∀x : set, x ∈ (X ∖ V) → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ A → apply_fun f0 x = 1).
An exact proof term for the current goal is (Urysohn_lemma X Tx (X ∖ V) A 0 1 H01 Hnorm HVcl HAcl Hdisj).
Apply HexU to the current goal.
Let f0 be given.
Assume Hf0: continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f0 ∧ (∀x : set, x ∈ (X ∖ V) → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ A → apply_fun f0 x = 1).
We prove the intermediate claim Hf0pair: continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f0 ∧ (∀x : set, x ∈ (X ∖ V) → apply_fun f0 x = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f0 ∧ (∀x : set, x ∈ (X ∖ V) → apply_fun f0 x = 0)) (∀x : set, x ∈ A → apply_fun f0 x = 1) Hf0).
We prove the intermediate claim Hf0cont: continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f0.
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f0) (∀x : set, x ∈ (X ∖ V) → apply_fun f0 x = 0) Hf0pair).
We prove the intermediate claim Hf0val0: ∀x : set, x ∈ (X ∖ V) → apply_fun f0 x = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f0) (∀x : set, x ∈ (X ∖ V) → apply_fun f0 x = 0) Hf0pair).
We prove the intermediate claim Hf0val1: ∀x : set, x ∈ A → apply_fun f0 x = 1.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f0 ∧ (∀x : set, x ∈ (X ∖ V) → apply_fun f0 x = 0)) (∀x : set, x ∈ A → apply_fun f0 x = 1) Hf0).
We prove the intermediate claim HclI_sub_R: closed_interval 0 1 ⊆ R.
Let r be given.
Assume Hr: r ∈ closed_interval 0 1.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) r Hr).
We prove the intermediate claim HTyEq: closed_interval_topology 0 1 = subspace_topology R R_standard_topology (closed_interval 0 1).
Use reflexivity.
We prove the intermediate claim Hf: continuous_map X Tx R R_standard_topology f0.
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 f0 Hf0cont HclI_sub_R R_standard_topology_is_topology_local HTyEq).
We use f0 to witness the existential quantifier.
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 Hf.
Let x be given.
Assume HxA: x ∈ A.
An exact proof term for the current goal is (Hf0val1 x HxA).
Let x be given.
Assume HxOut: x ∈ (X ∖ V).
An exact proof term for the current goal is (Hf0val0 x HxOut).
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun f0 x ∈ unit_interval.
We prove the intermediate claim Hfun: function_on f0 X (closed_interval 0 1).
An exact proof term for the current goal is (continuous_map_function_on X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f0 Hf0cont).
We prove the intermediate claim Himg: apply_fun f0 x ∈ closed_interval 0 1.
An exact proof term for the current goal is (Hfun x HxX).
We prove the intermediate claim HIeq: closed_interval 0 1 = unit_interval.
Use reflexivity.
rewrite the current goal using HIeq (from right to left).
An exact proof term for the current goal is Himg.
∎