Let X, Tx, x and U be given.
Assume Hcr: completely_regular_space X Tx.
Assume HxX: x ∈ X.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove ∃h : set, continuous_map X Tx unit_interval unit_interval_topology h ∧ apply_fun h x = 1 ∧ ∀y : set, y ∈ X ∖ U → apply_fun h y = 0.
We prove the intermediate claim Hex: ∃g : set, continuous_map X Tx R R_standard_topology g ∧ apply_fun g x = 1 ∧ ∀y : set, y ∈ X ∖ U → apply_fun g y = 0.
An exact proof term for the current goal is (completely_regular_space_open_separator X Tx x U Hcr HxX HU HxU).
Apply Hex to the current goal.
Let g be given.
Assume Hgpack: continuous_map X Tx R R_standard_topology g ∧ apply_fun g x = 1 ∧ ∀y : set, y ∈ X ∖ U → apply_fun g y = 0.
We use (compose_fun X g normalize01_fun) to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim Hgpair: (continuous_map X Tx R R_standard_topology g ∧ apply_fun g x = 1).
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology g ∧ apply_fun g x = 1) (∀y : set, y ∈ X ∖ U → apply_fun g y = 0) Hgpack).
We prove the intermediate claim Hgcont: continuous_map X Tx R R_standard_topology g.
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology g) (apply_fun g x = 1) Hgpair).
We prove the intermediate claim Hnorm: continuous_map R R_standard_topology unit_interval unit_interval_topology normalize01_fun.
An exact proof term for the current goal is normalize01_fun_continuous_to_unit_interval.
An exact proof term for the current goal is (composition_continuous X Tx R R_standard_topology unit_interval unit_interval_topology g normalize01_fun Hgcont Hnorm).
We prove the intermediate claim Hgpair: (continuous_map X Tx R R_standard_topology g ∧ apply_fun g x = 1).
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology g ∧ apply_fun g x = 1) (∀y : set, y ∈ X ∖ U → apply_fun g y = 0) Hgpack).
We prove the intermediate claim Hgx1: apply_fun g x = 1.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology g) (apply_fun g x = 1) Hgpair).
We prove the intermediate claim Happ: apply_fun (compose_fun X g normalize01_fun) x = apply_fun normalize01_fun (apply_fun g x).
An exact proof term for the current goal is (compose_fun_apply X g normalize01_fun x HxX).
rewrite the current goal using Happ (from left to right).
rewrite the current goal using Hgx1 (from left to right).
An exact proof term for the current goal is normalize01_fun_1.
Let y be given.
Assume HyOut: y ∈ X ∖ U.
We will prove apply_fun (compose_fun X g normalize01_fun) y = 0.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (y ∉ U) (setminusE X U y HyOut)).
We prove the intermediate claim Hgzero: ∀y0 : set, y0 ∈ X ∖ U → apply_fun g y0 = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology g ∧ apply_fun g x = 1) (∀y0 : set, y0 ∈ X ∖ U → apply_fun g y0 = 0) Hgpack).
We prove the intermediate claim Hgy0: apply_fun g y = 0.
An exact proof term for the current goal is (Hgzero y HyOut).
We prove the intermediate claim Happ: apply_fun (compose_fun X g normalize01_fun) y = apply_fun normalize01_fun (apply_fun g y).
An exact proof term for the current goal is (compose_fun_apply X g normalize01_fun y HyX).
rewrite the current goal using Happ (from left to right).
rewrite the current goal using Hgy0 (from left to right).
An exact proof term for the current goal is normalize01_fun_0.
∎