Let X, Tx and U be given.
Assume Hnorm: normal_space X Tx.
Assume HclosedG: ∀C : set, closed_in X Tx C → Gdelta_simple X Tx C.
Assume HUtx: U ∈ Tx.
We will prove ∃f0 : set, continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ X ∖ U → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ U → Rlt 0 (apply_fun f0 x)).
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 HUpow: U ∈ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx U HUtx).
We prove the intermediate claim HUsubX: U ⊆ X.
Let x be given.
Assume HxU: x ∈ U.
An exact proof term for the current goal is (PowerE X U HUpow x HxU).
Set A to be the term X ∖ U.
We prove the intermediate claim HAclosed: closed_in X Tx A.
An exact proof term for the current goal is (closed_of_open_complement X Tx U HTx HUtx).
We prove the intermediate claim HAgd: Gdelta_simple X Tx A.
An exact proof term for the current goal is (HclosedG A HAclosed).
We prove the intermediate claim Hexf0: ∃f0 : set, continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ A → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ X → x ∉ A → Rlt 0 (apply_fun f0 x)).
An exact proof term for the current goal is (lemma40_2_closed_Gdelta_has_positive_function X Tx A Hnorm HAclosed HAgd).
Apply Hexf0 to the current goal.
Let f0 be given.
Assume Hf0pack: continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ A → apply_fun f0 x = 0) ∧ (∀x : set, x ∈ X → x ∉ A → Rlt 0 (apply_fun f0 x)).
We prove the intermediate claim Hf0AB: continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ A → apply_fun f0 x = 0).
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ A → apply_fun f0 x = 0)) (∀x : set, x ∈ X → x ∉ A → Rlt 0 (apply_fun f0 x)) Hf0pack).
We prove the intermediate claim Hf0cont: continuous_map X Tx unit_interval unit_interval_topology f0.
An exact proof term for the current goal is (andEL (continuous_map X Tx unit_interval unit_interval_topology f0) (∀x : set, x ∈ A → apply_fun f0 x = 0) Hf0AB).
We prove the intermediate claim Hf0zeroA: ∀x : set, x ∈ A → apply_fun f0 x = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx unit_interval unit_interval_topology f0) (∀x : set, x ∈ A → apply_fun f0 x = 0) Hf0AB).
We prove the intermediate claim Hf0posOutA: ∀x : set, x ∈ X → x ∉ A → Rlt 0 (apply_fun f0 x).
An exact proof term for the current goal is (andER (continuous_map X Tx unit_interval unit_interval_topology f0 ∧ (∀x : set, x ∈ A → apply_fun f0 x = 0)) (∀x : set, x ∈ X → x ∉ A → Rlt 0 (apply_fun f0 x)) Hf0pack).
We use f0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hf0cont.
Let x be given.
Assume HxOut: x ∈ X ∖ U.
We will prove apply_fun f0 x = 0.
We prove the intermediate claim HxA: x ∈ A.
We prove the intermediate claim HdefA: A = X ∖ U.
Use reflexivity.
rewrite the current goal using HdefA (from left to right).
An exact proof term for the current goal is HxOut.
An exact proof term for the current goal is (Hf0zeroA x HxA).
Let x be given.
Assume HxU: x ∈ U.
We will prove Rlt 0 (apply_fun f0 x).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsubX x HxU).
We prove the intermediate claim HxnotA: x ∉ A.
Assume HxA: x ∈ A.
We prove the intermediate claim HxnotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 X U x HxA).
An exact proof term for the current goal is (HxnotU HxU).
An exact proof term for the current goal is (Hf0posOutA x HxX HxnotA).
∎