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 ∃f : set, f ∈ function_space X R ∧ continuous_map X Tx R R_standard_topology f ∧ (∀x : set, x ∈ X ∖ U → apply_fun f x = 0) ∧ (∀x : set, x ∈ U → Rlt 0 (apply_fun f 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 Hf0zero: ∀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 Hf0pos: ∀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).
Set f to be the term graph X (λx : set ⇒ apply_fun f0 x).
We use f to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply (graph_in_function_space X R (λx : set ⇒ apply_fun f0 x)) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun f0 x ∈ R.
We prove the intermediate claim Hf0fun: function_on f0 X unit_interval.
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology f0 Hf0cont).
We prove the intermediate claim Hf0xI: apply_fun f0 x ∈ unit_interval.
An exact proof term for the current goal is (Hf0fun x HxX).
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun f0 x) Hf0xI).
We prove the intermediate claim Hf0top: topology_on unit_interval unit_interval_topology.
An exact proof term for the current goal is unit_interval_topology_on.
We prove the intermediate claim HfcontI: continuous_map X Tx unit_interval unit_interval_topology f.
We will prove continuous_map X Tx unit_interval unit_interval_topology f.
We prove the intermediate claim HdefCM: continuous_map X Tx unit_interval unit_interval_topology f = (topology_on X Tx ∧ topology_on unit_interval unit_interval_topology ∧ function_on f X unit_interval ∧ ∀V : set, V ∈ unit_interval_topology → preimage_of X f V ∈ Tx).
Use reflexivity.
rewrite the current goal using HdefCM (from left to right).
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 HTx.
An exact proof term for the current goal is Hf0top.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun f x ∈ unit_interval.
We prove the intermediate claim Happ: apply_fun f x = apply_fun f0 x.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ apply_fun f0 x0) x HxX) (from left to right).
Use reflexivity.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (continuous_map_function_on X Tx unit_interval unit_interval_topology f0 Hf0cont x HxX).
Let V be given.
Assume HV: V ∈ unit_interval_topology.
We will prove preimage_of X f V ∈ Tx.
We prove the intermediate claim HpreEq: preimage_of X f V = preimage_of X f0 V.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X f V.
We will prove x ∈ preimage_of X f0 V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ V) x Hx).
We prove the intermediate claim HxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ V) x Hx).
We prove the intermediate claim Happ: apply_fun f x = apply_fun f0 x.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ apply_fun f0 x0) x HxX) (from left to right).
Use reflexivity.
We prove the intermediate claim HxV0: apply_fun f0 x ∈ V.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is HxV.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f0 x0 ∈ V) x HxX HxV0).
Let x be given.
Assume Hx: x ∈ preimage_of X f0 V.
We will prove x ∈ preimage_of X f V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f0 x0 ∈ V) x Hx).
We prove the intermediate claim HxV: apply_fun f0 x ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f0 x0 ∈ V) x Hx).
We prove the intermediate claim Happ: apply_fun f x = apply_fun f0 x.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ apply_fun f0 x0) x HxX) (from left to right).
Use reflexivity.
We prove the intermediate claim HxVf: apply_fun f x ∈ V.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is HxV.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxX HxVf).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (continuous_map_preimage X Tx unit_interval unit_interval_topology f0 Hf0cont V HV).
We prove the intermediate claim HsubI: unit_interval ⊆ R.
An exact proof term for the current goal is unit_interval_sub_R.
We prove the intermediate claim HTyR: 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 HTi: unit_interval_topology = subspace_topology R R_standard_topology unit_interval.
Use reflexivity.
An exact proof term for the current goal is (continuous_map_range_expand X Tx unit_interval unit_interval_topology R R_standard_topology f HfcontI HsubI HTyR HTi).
Let x be given.
Assume HxA: x ∈ X ∖ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X U x HxA).
We prove the intermediate claim Happ: apply_fun f x = apply_fun f0 x.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ apply_fun f0 x0) x HxX) (from left to right).
Use reflexivity.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (Hf0zero x HxA).
Let x be given.
Assume HxU: x ∈ U.
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).
We prove the intermediate claim Happ: apply_fun f x = apply_fun f0 x.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ apply_fun f0 x0) x HxX) (from left to right).
Use reflexivity.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (Hf0pos x HxX HxnotA).
∎