We will prove continuous_map (setprod R R) (product_topology R R_standard_topology R R_standard_topology) R R_standard_topology mul_fun_R.
Set Tx to be the term product_topology R R_standard_topology R R_standard_topology.
Set S to be the term open_rays_subbasis R.
We prove the intermediate claim HTx: topology_on (setprod R R) Tx.
An exact proof term for the current goal is (product_topology_is_topology R R_standard_topology R R_standard_topology R_standard_topology_is_topology_local R_standard_topology_is_topology_local).
We prove the intermediate claim Hfun: function_on mul_fun_R (setprod R R) R.
Let p be given.
Assume HpRR: p ∈ setprod R R.
An exact proof term for the current goal is (mul_fun_R_value_in_R p HpRR).
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 = R_standard_topology.
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.
We prove the intermediate claim HpreS: ∀s : set, s ∈ S → preimage_of (setprod R R) mul_fun_R s ∈ Tx.
Let s be given.
Assume HsS: s ∈ S.
We will prove preimage_of (setprod R R) mul_fun_R s ∈ Tx.
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 (setprod R R) mul_fun_R s ∈ Tx)) to the current goal.
Assume Hs0: 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 (setprod R R) mul_fun_R s ∈ Tx)) to the current goal.
Assume Hsu: 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 Hsu).
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 (preimage_mul_fun_R_open_ray_upper_in_product_topology a HaR).
Assume Hsl: 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 Hsl).
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 (preimage_mul_fun_R_open_ray_lower_in_product_topology b HbR).
An exact proof term for the current goal is Hs0.
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).
We prove the intermediate claim Heq: preimage_of (setprod R R) mul_fun_R R = setprod R R.
An exact proof term for the current goal is (preimage_of_whole (setprod R R) R mul_fun_R Hfun).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_has_X (setprod R R) Tx HTx).
An exact proof term for the current goal is HsS.
We prove the intermediate claim Hcont0: continuous_map (setprod R R) Tx R (generated_topology_from_subbasis R S) mul_fun_R.
An exact proof term for the current goal is (continuous_map_from_subbasis (setprod R R) Tx R S mul_fun_R HTx Hfun HS HpreS).
We prove the intermediate claim Hsub: R_standard_topology ⊆ generated_topology_from_subbasis R S.
rewrite the current goal using Hgen (from right to left).
Let U be given.
Assume HU: U ∈ generated_topology_from_subbasis R S.
An exact proof term for the current goal is HU.
An exact proof term for the current goal is (continuous_map_codomain_coarser (setprod R R) Tx R (generated_topology_from_subbasis R S) R_standard_topology mul_fun_R Hcont0 R_standard_topology_is_topology_local Hsub).
∎