Let X, Tx and f be given.
Assume HTx: topology_on X Tx.
Assume Hf: continuous_map X Tx R R_standard_topology f.
Assume Hpos: ∀x : set, x ∈ X → Rlt 0 (apply_fun f x).
We will prove continuous_map X Tx R R_standard_topology (compose_fun X f (compose_fun (open_ray_upper R 0) (compose_fun R bounded_transform_phi one_minus_fun) bounded_transform_psi)).
Set Ipos to be the term open_ray_upper R 0.
Set Tpos to be the term subspace_topology R R_standard_topology Ipos.
Set r to be the term compose_fun Ipos (compose_fun R bounded_transform_phi one_minus_fun) bounded_transform_psi.
We prove the intermediate claim HIposSubR: Ipos ⊆ R.
Let t be given.
Assume HtIpos: t ∈ Ipos.
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ order_rel R 0 x) t HtIpos).
We prove the intermediate claim Himg: ∀x : set, x ∈ X → apply_fun f x ∈ Ipos.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HfxR: apply_fun f x ∈ R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology f Hf x HxX).
We prove the intermediate claim H0ltfx: Rlt 0 (apply_fun f x).
An exact proof term for the current goal is (Hpos x HxX).
We prove the intermediate claim Hrel: order_rel R 0 (apply_fun f x).
An exact proof term for the current goal is (Rlt_implies_order_rel_R 0 (apply_fun f x) H0ltfx).
An exact proof term for the current goal is (SepI R (λy : set ⇒ order_rel R 0 y) (apply_fun f x) HfxR Hrel).
We prove the intermediate claim Hf_to_pos: continuous_map X Tx Ipos Tpos f.
An exact proof term for the current goal is (continuous_map_range_restrict X Tx R R_standard_topology f Ipos Hf HIposSubR Himg).
We prove the intermediate claim Hr: continuous_map Ipos Tpos R R_standard_topology r.
An exact proof term for the current goal is recip_pos_continuous_via_bounded_transforms.
An exact proof term for the current goal is (composition_continuous X Tx Ipos Tpos R R_standard_topology f r Hf_to_pos Hr).
∎