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) ∧ support_of X Tx f ⊆ closure_of X Tx V.
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 Hexf: ∃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).
An exact proof term for the current goal is (Urysohn_bump_closed_in_open X Tx A V Hnorm HAcl HVopen HAsubV).
Apply Hexf to the current goal.
Let f be given.
Assume Hfpack: 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 use f to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim H123: (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).
An exact proof term for the current goal is Hfpack.
We prove the intermediate claim Hcm_p1_p2: 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).
An exact proof term for the current goal is (andEL (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) H123).
We prove the intermediate claim Hp3: ∀x : set, x ∈ X → apply_fun f x ∈ unit_interval.
An exact proof term for the current goal is (andER (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) H123).
We prove the intermediate claim Hcm_p1: (continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ A → apply_fun f x = 1)).
An exact proof term for the current goal is (andEL (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) Hcm_p1_p2).
We prove the intermediate claim Hcm: 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) (∀x : set, x ∈ A → apply_fun f x = 1) Hcm_p1).
We prove the intermediate claim Hp1: ∀x : set, x ∈ A → apply_fun f x = 1.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology f) (∀x : set, x ∈ A → apply_fun f x = 1) Hcm_p1).
We prove the intermediate claim Hp2: ∀x : set, x ∈ (X ∖ V) → apply_fun f x = 0.
An exact proof term for the current goal is (andER (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) Hcm_p1_p2).
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 Hcm.
An exact proof term for the current goal is Hp1.
An exact proof term for the current goal is Hp2.
An exact proof term for the current goal is Hp3.
We prove the intermediate claim Hz: ∀x : set, x ∈ (X ∖ V) → apply_fun f x = 0.
We prove the intermediate claim Hcm_p1_p2: 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).
An exact proof term for the current goal is (andEL (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) Hfpack).
An exact proof term for the current goal is (andER (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) Hcm_p1_p2).
An exact proof term for the current goal is (support_of_zero_outside_open_sub_closure X Tx f V HTx HVopen Hz).
∎