Let X, Tx, A, a, b and f be given.
Assume Hab: Rle a b.
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.
Assume HfI: ∀x : set, x ∈ A → apply_fun f x ∈ closed_interval a b.
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).
Set I to be the term closed_interval a b.
Set Ti to be the term closed_interval_topology a b.
We prove the intermediate claim HIsubR: I ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R a b).
We prove the intermediate claim Hf_to_I: continuous_map A (subspace_topology X Tx A) I Ti f.
We prove the intermediate claim HfRng: continuous_map A (subspace_topology X Tx A) I (subspace_topology R R_standard_topology I) f.
An exact proof term for the current goal is (continuous_map_range_restrict A (subspace_topology X Tx A) R R_standard_topology f I Hf HIsubR HfI).
An exact proof term for the current goal is HfRng.
We prove the intermediate claim HexgI: ∃gI : set, continuous_map X Tx I Ti gI ∧ (∀x : set, x ∈ A → apply_fun gI x = apply_fun f x).
An exact proof term for the current goal is (Tietze_extension_interval X Tx A a b f Hab Hnorm HA Hf_to_I).
Apply HexgI to the current goal.
Let gI be given.
Assume HgI.
We prove the intermediate claim HgIcont: continuous_map X Tx I Ti gI.
An exact proof term for the current goal is (andEL (continuous_map X Tx I Ti gI) (∀x : set, x ∈ A → apply_fun gI x = apply_fun f x) HgI).
We prove the intermediate claim HgIeq: ∀x : set, x ∈ A → apply_fun gI x = apply_fun f x.
An exact proof term for the current goal is (andER (continuous_map X Tx I Ti gI) (∀x : set, x ∈ A → apply_fun gI x = apply_fun f x) HgI).
Set inc to be the term {(y,y)|y ∈ I}.
We prove the intermediate claim Hinc: continuous_map I Ti R R_standard_topology inc.
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 (subspace_inclusion_continuous R R_standard_topology I HRtop HIsubR).
Set g to be the term compose_fun X gI inc.
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 I Ti R R_standard_topology gI inc HgIcont Hinc).
Let x be given.
Assume HxA: x ∈ A.
We will prove apply_fun g x = apply_fun f x.
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HA).
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 Hcomp: apply_fun g x = apply_fun inc (apply_fun gI x).
rewrite the current goal using (compose_fun_apply X gI inc x HxX) (from left to right).
Use reflexivity.
rewrite the current goal using Hcomp (from left to right).
We prove the intermediate claim HgIxI: apply_fun gI x ∈ I.
An exact proof term for the current goal is (continuous_map_function_on X Tx I Ti gI HgIcont x HxX).
We prove the intermediate claim HincId: apply_fun inc (apply_fun gI x) = apply_fun gI x.
An exact proof term for the current goal is (identity_function_apply I (apply_fun gI x) HgIxI).
rewrite the current goal using HincId (from left to right).
An exact proof term for the current goal is (HgIeq x HxA).
∎