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 ∃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.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (one_point_sets_closed X Tx ∧ ∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x0 = 0 ∧ ∀y : set, y ∈ F0 → apply_fun f y = 1) Hcr).
Set F to be the term X ∖ U.
We prove the intermediate claim HFcl: closed_in X Tx F.
An exact proof term for the current goal is (closed_of_open_complement X Tx U HTx HU).
We prove the intermediate claim HxnotF: x ∉ F.
Assume HxF: x ∈ F.
We prove the intermediate claim HxU': x ∉ U.
An exact proof term for the current goal is (andER (x ∈ X) (x ∉ U) (setminusE X U x HxF)).
An exact proof term for the current goal is (HxU' HxU).
We prove the intermediate claim Hrest: one_point_sets_closed X Tx ∧ ∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x0 = 0 ∧ ∀y : set, y ∈ F0 → apply_fun f y = 1.
An exact proof term for the current goal is (andER (topology_on X Tx) (one_point_sets_closed X Tx ∧ ∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x0 = 0 ∧ ∀y : set, y ∈ F0 → apply_fun f y = 1) Hcr).
We prove the intermediate claim Hsep: ∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x0 = 0 ∧ ∀y : set, y ∈ F0 → apply_fun f y = 1.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃f : set, continuous_map X Tx R R_standard_topology f ∧ apply_fun f x0 = 0 ∧ ∀y : set, y ∈ F0 → apply_fun f y = 1) Hrest).
Apply (Hsep x HxX F HFcl HxnotF) to the current goal.
Let f be given.
Assume Hfpack: continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1.
We prove the intermediate claim Hcontf: continuous_map X Tx R R_standard_topology f.
We prove the intermediate claim Hpair: continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0.
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0) (∀y : set, y ∈ F → apply_fun f y = 1) Hfpack).
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology f) (apply_fun f x = 0) Hpair).
We prove the intermediate claim Hfx0: apply_fun f x = 0.
We prove the intermediate claim Hpair: continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0.
An exact proof term for the current goal is (andEL (continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0) (∀y : set, y ∈ F → apply_fun f y = 1) Hfpack).
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology f) (apply_fun f x = 0) Hpair).
We prove the intermediate claim HfF1: ∀y : set, y ∈ F → apply_fun f y = 1.
An exact proof term for the current goal is (andER (continuous_map X Tx R R_standard_topology f ∧ apply_fun f x = 0) (∀y : set, y ∈ F → apply_fun f y = 1) Hfpack).
We use (compose_fun X f one_minus_fun) to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim Hone: continuous_map R R_standard_topology R R_standard_topology one_minus_fun.
An exact proof term for the current goal is one_minus_fun_continuous.
An exact proof term for the current goal is (composition_continuous X Tx R R_standard_topology R R_standard_topology f one_minus_fun Hcontf Hone).
We will prove apply_fun (compose_fun X f one_minus_fun) x = 1.
We prove the intermediate claim Hgx: apply_fun (compose_fun X f one_minus_fun) x = apply_fun one_minus_fun (apply_fun f x).
An exact proof term for the current goal is (compose_fun_apply X f one_minus_fun x HxX).
rewrite the current goal using Hgx (from left to right).
rewrite the current goal using Hfx0 (from left to right).
An exact proof term for the current goal is one_minus_fun_0.
Let y be given.
Assume HyF: y ∈ X ∖ U.
We will prove apply_fun (compose_fun X f one_minus_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 HyF)).
We prove the intermediate claim Hgy: apply_fun (compose_fun X f one_minus_fun) y = apply_fun one_minus_fun (apply_fun f y).
An exact proof term for the current goal is (compose_fun_apply X f one_minus_fun y HyX).
rewrite the current goal using Hgy (from left to right).
rewrite the current goal using (HfF1 y HyF) (from left to right).
An exact proof term for the current goal is one_minus_fun_1.
∎