We will prove continuous_map (open_interval (minus_SNo 1) 1) (subspace_topology R R_standard_topology (open_interval (minus_SNo 1) 1)) R R_standard_topology bounded_transform_psi.
Set I to be the term open_interval (minus_SNo 1) 1.
Set Ti to be the term subspace_topology R R_standard_topology I.
Set S to be the term open_rays_subbasis R.
We prove the intermediate claim HI_sub_R: I ⊆ R.
Let x be given.
Assume HxI: x ∈ I.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) x HxI).
We prove the intermediate claim HTi: topology_on I Ti.
An exact proof term for the current goal is (subspace_topology_is_topology R R_standard_topology I R_standard_topology_is_topology HI_sub_R).
We prove the intermediate claim Hfun: function_on bounded_transform_psi I R.
Let s be given.
Assume HsI: s ∈ I.
We will prove apply_fun bounded_transform_psi s ∈ R.
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (HI_sub_R s HsI).
We prove the intermediate claim HabsR: abs_SNo s ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R s HsR).
We prove the intermediate claim HminR: minus_SNo (abs_SNo s) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (abs_SNo s) HabsR).
We prove the intermediate claim HdenR: add_SNo 1 (minus_SNo (abs_SNo s)) ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo (abs_SNo s)) HminR).
We prove the intermediate claim HpsiDef: bounded_transform_psi = graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))).
Use reflexivity.
rewrite the current goal using HpsiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))) s HsR) (from left to right).
An exact proof term for the current goal is (real_div_SNo s HsR (add_SNo 1 (minus_SNo (abs_SNo s))) HdenR).
We prove the intermediate claim HS: subbasis_on R S.
An exact proof term for the current goal is (open_rays_subbasis_is_subbasis R).
We prove the intermediate claim HTyEq: R_standard_topology = generated_topology_from_subbasis R S.
We prove the intermediate claim HSdef0: S = open_rays_subbasis R.
Use reflexivity.
rewrite the current goal using HSdef0 (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from right to left).
rewrite the current goal using open_rays_subbasis_for_order_topology_R (from right to left).
Use reflexivity.
rewrite the current goal using HTyEq (from left to right) at position 2.
Apply (continuous_map_from_subbasis I Ti R S bounded_transform_psi HTi Hfun HS) to the current goal.
Let s be given.
Assume HsS: s ∈ S.
We will prove preimage_of I bounded_transform_psi s ∈ Ti.
We prove the intermediate claim HSdef: S = (({I0 ∈ 𝒫 R|∃a ∈ R, I0 = open_ray_upper R a} ∪ {I0 ∈ 𝒫 R|∃b ∈ R, I0 = open_ray_lower R b}) ∪ {R}).
Use reflexivity.
We prove the intermediate claim HsS': s ∈ (({I0 ∈ 𝒫 R|∃a ∈ R, I0 = open_ray_upper R a} ∪ {I0 ∈ 𝒫 R|∃b ∈ R, I0 = open_ray_lower R b}) ∪ {R}).
rewrite the current goal using HSdef (from right to left).
An exact proof term for the current goal is HsS.
Apply (binunionE' ({I0 ∈ 𝒫 R|∃a ∈ R, I0 = open_ray_upper R a} ∪ {I0 ∈ 𝒫 R|∃b ∈ R, I0 = open_ray_lower R b}) {R} s (preimage_of I bounded_transform_psi s ∈ Ti)) to the current goal.
Assume HsAB: s ∈ ({I0 ∈ 𝒫 R|∃a ∈ R, I0 = open_ray_upper R a} ∪ {I0 ∈ 𝒫 R|∃b ∈ R, I0 = open_ray_lower R b}).
Apply (binunionE' {I0 ∈ 𝒫 R|∃a ∈ R, I0 = open_ray_upper R a} {I0 ∈ 𝒫 R|∃b ∈ R, I0 = open_ray_lower R b} s (preimage_of I bounded_transform_psi s ∈ Ti)) to the current goal.
Assume HsUpper: s ∈ {I0 ∈ 𝒫 R|∃a ∈ R, I0 = open_ray_upper R a}.
We prove the intermediate claim Hex: ∃a ∈ R, s = open_ray_upper R a.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI1 : set ⇒ ∃a ∈ R, I1 = open_ray_upper R a) s HsUpper).
Apply Hex to the current goal.
Let a be given.
Assume Hacore.
Apply Hacore to the current goal.
Assume HaR: a ∈ R.
Assume Hseq: s = open_ray_upper R a.
rewrite the current goal using Hseq (from left to right).
An exact proof term for the current goal is (bounded_transform_psi_preimage_open_ray_upper a HaR).
Assume HsLower: s ∈ {I0 ∈ 𝒫 R|∃b ∈ R, I0 = open_ray_lower R b}.
We prove the intermediate claim Hex: ∃b ∈ R, s = open_ray_lower R b.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI1 : set ⇒ ∃b ∈ R, I1 = open_ray_lower R b) s HsLower).
Apply Hex to the current goal.
Let b be given.
Assume Hbcore.
Apply Hbcore to the current goal.
Assume HbR: b ∈ R.
Assume Hseq: s = open_ray_lower R b.
rewrite the current goal using Hseq (from left to right).
An exact proof term for the current goal is (bounded_transform_psi_preimage_open_ray_lower b HbR).
An exact proof term for the current goal is HsAB.
Assume HsR: s ∈ {R}.
We prove the intermediate claim Hseq: s = R.
An exact proof term for the current goal is (SingE R s HsR).
rewrite the current goal using Hseq (from left to right).
rewrite the current goal using (preimage_of_whole I R bounded_transform_psi Hfun) (from left to right).
An exact proof term for the current goal is (topology_has_X I Ti HTi).
An exact proof term for the current goal is HsS'.
∎