Let X, Tx, A, B and U be given.
Assume Hnorm: normal_space X Tx.
Assume HAcl: closed_in X Tx A.
Assume HBcl: closed_in X Tx B.
Assume HAB: A ∩ B = Empty.
We will prove ∃f : set, continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ A → apply_fun f x = 0) ∧ (∀x : set, x ∈ B → apply_fun f x = 1).
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).
Apply (Urysohn_lemma X Tx A B 0 1 H0le1 Hnorm HAcl HBcl HAB) to the current goal.
Let f be given.
Assume Hfpack.
We use f to witness the existential quantifier.
We will prove continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ A → apply_fun f x = 0) ∧ (∀x : set, x ∈ B → apply_fun f x = 1).
We prove the intermediate claim Hcore: (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀x : set, x ∈ A → apply_fun f 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) f ∧ (∀x : set, x ∈ A → apply_fun f x = 0)) (∀x : set, x ∈ B → apply_fun f x = 1) Hfpack).
We prove the intermediate claim HfB: ∀x : set, x ∈ B → apply_fun f 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) f ∧ (∀x : set, x ∈ A → apply_fun f x = 0)) (∀x : set, x ∈ B → apply_fun f x = 1) Hfpack).
We prove the intermediate claim HfcontI: 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) (∀x : set, x ∈ A → apply_fun f x = 0) Hcore).
We prove the intermediate claim HfA: ∀x : set, x ∈ A → apply_fun f 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) f) (∀x : set, x ∈ A → apply_fun f x = 0) Hcore).
We prove the intermediate claim HI_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 HTyEq: 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 HfcontI HI_sub_R HTstd HTyEq).
Apply andI to the current goal.
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 HfA.
An exact proof term for the current goal is HfB.
∎