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) R R_standard_topology f.
We will prove ∃g : set, continuous_map X Tx R R_standard_topology g ∧ (∀x : set, x ∈ A → apply_fun g x = apply_fun f x).
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 (∃g : set, continuous_map X Tx R R_standard_topology g ∧ (∀x : set, x ∈ A → apply_fun g x = apply_fun f x))) to the current goal.
Assume HAemp: A = Empty.
We use (const_fun X 0) to witness the existential quantifier.
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).
We prove the intermediate claim HRtop: topology_on R R_standard_topology.
An exact proof term for the current goal is (R_standard_topology_is_topology_local).
An exact proof term for the current goal is (const_fun_continuous X Tx R R_standard_topology 0 HTx HRtop real_0).
Let x be given.
Assume HxA: x ∈ A.
We will prove apply_fun (const_fun X 0) x = apply_fun f x.
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.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE x) HxE).
Assume HAne: ¬ (A = Empty).
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 HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HA).
Set J to be the term open_interval (minus_SNo 1) 1.
Set Tj to be the term subspace_topology R R_standard_topology J.
Set phi to be the term bounded_transform_phi.
We prove the intermediate claim Hphi_cont: continuous_map R R_standard_topology R R_standard_topology phi.
We prove the intermediate claim HphiDef: phi = bounded_transform_phi.
Use reflexivity.
rewrite the current goal using HphiDef (from left to right).
An exact proof term for the current goal is bounded_transform_phi_continuous.
Set h to be the term compose_fun A f phi.
We prove the intermediate claim Hh_cont_R: continuous_map A (subspace_topology X Tx A) R R_standard_topology h.
An exact proof term for the current goal is (composition_continuous A (subspace_topology X Tx A) R R_standard_topology R R_standard_topology f phi Hf Hphi_cont).
We prove the intermediate claim HJsubR: J ⊆ R.
Let s be given.
Assume HsJ: s ∈ J.
An exact proof term for the current goal is (open_interval_Subq_R (minus_SNo 1) 1 s HsJ).
We prove the intermediate claim HhJimg: ∀x : set, x ∈ A → apply_fun h x ∈ J.
Let x be given.
Assume HxA: x ∈ A.
We will prove apply_fun h x ∈ J.
We prove the intermediate claim HxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (continuous_map_function_on A (subspace_topology X Tx A) R R_standard_topology f Hf x HxA).
We prove the intermediate claim Hhapp: apply_fun h x = apply_fun phi (apply_fun f x).
rewrite the current goal using (compose_fun_apply A f phi x HxA) (from left to right).
Use reflexivity.
rewrite the current goal using Hhapp (from left to right).
We prove the intermediate claim HphiDef: phi = bounded_transform_phi.
Use reflexivity.
rewrite the current goal using HphiDef (from left to right).
We prove the intermediate claim Hbnds: Rlt (minus_SNo 1) (apply_fun bounded_transform_phi (apply_fun f x)) ∧ Rlt (apply_fun bounded_transform_phi (apply_fun f x)) 1.
An exact proof term for the current goal is (bounded_transform_phi_strict_bounds (apply_fun f x) HxR).
We prove the intermediate claim Hltm1: Rlt (minus_SNo 1) (apply_fun bounded_transform_phi (apply_fun f x)).
An exact proof term for the current goal is (andEL (Rlt (minus_SNo 1) (apply_fun bounded_transform_phi (apply_fun f x))) (Rlt (apply_fun bounded_transform_phi (apply_fun f x)) 1) Hbnds).
We prove the intermediate claim Hlt1: Rlt (apply_fun bounded_transform_phi (apply_fun f x)) 1.
An exact proof term for the current goal is (andER (Rlt (minus_SNo 1) (apply_fun bounded_transform_phi (apply_fun f x))) (Rlt (apply_fun bounded_transform_phi (apply_fun f x)) 1) Hbnds).
We prove the intermediate claim HyR: apply_fun bounded_transform_phi (apply_fun f x) ∈ R.
An exact proof term for the current goal is (bounded_transform_phi_value_in_R (apply_fun f x) HxR).
We prove the intermediate claim HJdef: J = {z ∈ R|Rlt (minus_SNo 1) z ∧ Rlt z 1}.
Use reflexivity.
rewrite the current goal using HJdef (from left to right).
Apply (SepI R (λz : set ⇒ Rlt (minus_SNo 1) z ∧ Rlt z 1) (apply_fun bounded_transform_phi (apply_fun f x)) HyR) to the current goal.
An exact proof term for the current goal is (andI (Rlt (minus_SNo 1) (apply_fun bounded_transform_phi (apply_fun f x))) (Rlt (apply_fun bounded_transform_phi (apply_fun f x)) 1) Hltm1 Hlt1).
We prove the intermediate claim Hh_cont_J: continuous_map A (subspace_topology X Tx A) J Tj h.
An exact proof term for the current goal is (continuous_map_range_restrict A (subspace_topology X Tx A) R R_standard_topology h J Hh_cont_R HJsubR HhJimg).
We prove the intermediate claim HexgJ: ∃gJ : set, continuous_map X Tx J Tj gJ ∧ (∀x : set, x ∈ A → apply_fun gJ x = apply_fun h x).
An exact proof term for the current goal is (Tietze_extension_open_interval X Tx A h Hnorm HA Hh_cont_J).
Apply HexgJ to the current goal.
Let gJ be given.
Assume HgJ.
We prove the intermediate claim HgJ_cont: continuous_map X Tx J Tj gJ.
An exact proof term for the current goal is (andEL (continuous_map X Tx J Tj gJ) (∀x : set, x ∈ A → apply_fun gJ x = apply_fun h x) HgJ).
We prove the intermediate claim HgJ_eq: ∀x : set, x ∈ A → apply_fun gJ x = apply_fun h x.
An exact proof term for the current goal is (andER (continuous_map X Tx J Tj gJ) (∀x : set, x ∈ A → apply_fun gJ x = apply_fun h x) HgJ).
Set psi to be the term bounded_transform_psi.
We prove the intermediate claim Hpsi_cont: continuous_map J Tj R R_standard_topology psi.
An exact proof term for the current goal is bounded_transform_psi_continuous_open_interval.
Set g to be the term compose_fun X gJ psi.
We use g to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (composition_continuous X Tx J Tj R R_standard_topology gJ psi HgJ_cont Hpsi_cont).
Let x be given.
Assume HxA: x ∈ A.
We will prove apply_fun g x = apply_fun f x.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate claim Hgapp: apply_fun g x = apply_fun psi (apply_fun gJ x).
rewrite the current goal using (compose_fun_apply X gJ psi x HxX) (from left to right).
Use reflexivity.
rewrite the current goal using Hgapp (from left to right).
rewrite the current goal using (HgJ_eq x HxA) (from left to right).
We prove the intermediate claim HxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (continuous_map_function_on A (subspace_topology X Tx A) R R_standard_topology f Hf x HxA).
We prove the intermediate claim Hhapp: apply_fun h x = apply_fun bounded_transform_phi (apply_fun f x).
rewrite the current goal using (compose_fun_apply A f phi x HxA) (from left to right).
We prove the intermediate claim HphiDef: phi = bounded_transform_phi.
Use reflexivity.
rewrite the current goal using HphiDef (from left to right).
Use reflexivity.
rewrite the current goal using Hhapp (from left to right).
An exact proof term for the current goal is (bounded_transform_psi_phi_cancel (apply_fun f x) HxR).
∎