Let c be given.
Assume HcR: c ∈ R.
Assume Hcpos: 0 < c.
We will prove continuous_map R R_standard_topology R R_standard_topology (mul_const_fun c).
Set Tx to be the term R_standard_topology.
Set S to be the term open_rays_subbasis R.
We prove the intermediate claim HTx: topology_on R Tx.
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim Hfun: function_on (mul_const_fun c) R R.
Let t be given.
Assume HtR: t ∈ R.
An exact proof term for the current goal is (mul_const_fun_value_in_R c t HcR HtR).
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 Hgen: generated_topology_from_subbasis R S = Tx.
rewrite the current goal using open_rays_subbasis_for_order_topology_R (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from left to right).
Use reflexivity.
rewrite the current goal using Hgen (from right to left) at position 2.
Apply (continuous_map_from_subbasis R Tx R S (mul_const_fun c) HTx Hfun HS) to the current goal.
Let s be given.
Assume HsS: s ∈ S.
We will prove preimage_of R (mul_const_fun c) s ∈ Tx.
We prove the intermediate claim HSdef: S = (({I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a} ∪ {I ∈ 𝒫 R|∃b ∈ R, I = open_ray_lower R b}) ∪ {R}).
Use reflexivity.
We prove the intermediate claim HsS': s ∈ (({I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a} ∪ {I ∈ 𝒫 R|∃b ∈ R, I = 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' ({I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a} ∪ {I ∈ 𝒫 R|∃b ∈ R, I = open_ray_lower R b}) {R} s (preimage_of R (mul_const_fun c) s ∈ Tx)) to the current goal.
Assume HsAB: s ∈ ({I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a} ∪ {I ∈ 𝒫 R|∃b ∈ R, I = open_ray_lower R b}).
Apply (binunionE' {I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a} {I ∈ 𝒫 R|∃b ∈ R, I = open_ray_lower R b} s (preimage_of R (mul_const_fun c) s ∈ Tx)) to the current goal.
Assume HsUpper: s ∈ {I ∈ 𝒫 R|∃a ∈ R, I = 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) (λI0 : set ⇒ ∃a ∈ R, I0 = 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).
rewrite the current goal using (preimage_mul_const_open_ray_upper c a HcR Hcpos HaR) (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HdivR: div_SNo a c ∈ R.
An exact proof term for the current goal is (real_div_SNo a HaR c HcR).
We prove the intermediate claim Hray: open_ray_upper R (div_SNo a c) ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R (div_SNo a c) HdivR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_upper R (div_SNo a c)) Hray).
Assume HsLower: s ∈ {I ∈ 𝒫 R|∃b ∈ R, I = 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) (λI0 : set ⇒ ∃b ∈ R, I0 = 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).
rewrite the current goal using (preimage_mul_const_open_ray_lower c b HcR Hcpos HbR) (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HdivR: div_SNo b c ∈ R.
An exact proof term for the current goal is (real_div_SNo b HbR c HcR).
We prove the intermediate claim Hray: open_ray_lower R (div_SNo b c) ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis R (div_SNo b c) HdivR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_lower R (div_SNo b c)) Hray).
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 R R (mul_const_fun c) Hfun) (from left to right).
An exact proof term for the current goal is (topology_has_X R Tx HTx).
An exact proof term for the current goal is HsS'.
∎