Let X, Tx, A and f be given.
Assume Hnorm: normal_space X Tx.
Assume HA: closed_in X Tx A.
Assume Hf: continuous_map A (subspace_topology X Tx A) (closed_interval (minus_SNo 1) 1) (closed_interval_topology (minus_SNo 1) 1) f.
We will prove ∃gR : set, continuous_map X Tx R R_standard_topology gR ∧ (∀x : set, x ∈ A → apply_fun gR x = apply_fun f x) ∧ (∀x : set, x ∈ X → apply_fun gR x ∈ closed_interval (minus_SNo 1) 1).
We prove the intermediate claim HA_cases: A = Empty ∨ ¬ (A = Empty).
An exact proof term for the current goal is (xm (A = Empty)).
Apply (HA_cases (∃gR : set, continuous_map X Tx R R_standard_topology gR ∧ (∀x : set, x ∈ A → apply_fun gR x = apply_fun f x) ∧ (∀x : set, x ∈ X → apply_fun gR x ∈ closed_interval (minus_SNo 1) 1))) to the current goal.
Assume HAemp: A = Empty.
We use (const_fun X 0) to witness the existential quantifier.
We will prove continuous_map X Tx R R_standard_topology (const_fun X 0) ∧ (∀x : set, x ∈ A → apply_fun (const_fun X 0) x = apply_fun f x) ∧ (∀x : set, x ∈ X → apply_fun (const_fun X 0) x ∈ closed_interval (minus_SNo 1) 1).
Apply andI to the current goal.
Apply andI to the current goal.
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).
An exact proof term for the current goal is (const_fun_continuous X Tx R R_standard_topology 0 HTx R_standard_topology_is_topology_local real_0).
Let x be given.
Assume HxA: x ∈ A.
We will prove apply_fun (const_fun X 0) x = apply_fun f x.
Apply FalseE to the current goal.
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HAemp (from right to left).
An exact proof term for the current goal is HxA.
An exact proof term for the current goal is (EmptyE x HxE).
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun (const_fun X 0) x ∈ closed_interval (minus_SNo 1) 1.
rewrite the current goal using (const_fun_apply X 0 x HxX) (from left to right).
An exact proof term for the current goal is zero_in_closed_interval_minus1_1.
Assume HAnemp: ¬ (A = Empty).
An exact proof term for the current goal is (Tietze_stepII_real_extension_nonempty X Tx A f Hnorm HA HAnemp Hf).
∎