Let i be given.
Assume Hi: i ∈ ω.
We will prove continuous_map R_omega_space R_omega_product_topology R R_standard_topology (Romega_coord_map i).
Set Xi to be the term const_space_family ω R R_standard_topology.
Set S to be the term product_subbasis_full ω Xi.
We prove the intermediate claim HXdef: R_omega_space = product_space ω Xi.
Use reflexivity.
We prove the intermediate claim HtopX: topology_on R_omega_space R_omega_product_topology.
An exact proof term for the current goal is Romega_product_topology_is_topology.
We prove the intermediate claim HtopR: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim Hfun: function_on (Romega_coord_map i) R_omega_space R.
An exact proof term for the current goal is (Romega_coord_map_function_on i Hi).
We will prove topology_on R_omega_space R_omega_product_topology ∧ topology_on R R_standard_topology ∧ function_on (Romega_coord_map i) R_omega_space R ∧ ∀U : set, U ∈ R_standard_topology → preimage_of R_omega_space (Romega_coord_map i) U ∈ R_omega_product_topology.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HtopX.
An exact proof term for the current goal is HtopR.
An exact proof term for the current goal is Hfun.
Let U be given.
Assume HU: U ∈ R_standard_topology.
We will prove preimage_of R_omega_space (Romega_coord_map i) U ∈ R_omega_product_topology.
Set Cyl to be the term product_cylinder ω Xi i U.
We prove the intermediate claim HIne: ω ≠ Empty.
We prove the intermediate claim H0o: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
An exact proof term for the current goal is (elem_implies_nonempty ω 0 H0o).
We prove the intermediate claim HcompTop: ∀j : set, j ∈ ω → topology_on (space_family_set Xi j) (space_family_topology Xi j).
Let j be given.
Assume Hj: j ∈ ω.
We prove the intermediate claim HXi: apply_fun Xi j = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology j Hj).
We prove the intermediate claim Hset: space_family_set Xi j = R.
We prove the intermediate claim Hdef: space_family_set Xi j = (apply_fun Xi j) 0.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HXi (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq R R_standard_topology).
We prove the intermediate claim Htop: space_family_topology Xi j = R_standard_topology.
We prove the intermediate claim Hdef: space_family_topology Xi j = (apply_fun Xi j) 1.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HXi (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq R R_standard_topology).
rewrite the current goal using Hset (from left to right).
rewrite the current goal using Htop (from left to right).
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HS: subbasis_on R_omega_space S.
An exact proof term for the current goal is Romega_product_subbasis_on.
We prove the intermediate claim HUtop: U ∈ space_family_topology Xi i.
We prove the intermediate claim HXi0: apply_fun Xi i = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology i Hi).
We prove the intermediate claim Htopi: space_family_topology Xi i = R_standard_topology.
We prove the intermediate claim Hdef: space_family_topology Xi i = (apply_fun Xi i) 1.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HXi0 (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq R R_standard_topology).
rewrite the current goal using Htopi (from left to right).
An exact proof term for the current goal is HU.
We prove the intermediate claim HCylS: Cyl ∈ S.
We prove the intermediate claim HCylRepl: Cyl ∈ {product_cylinder ω Xi i U0|U0 ∈ space_family_topology Xi i}.
An exact proof term for the current goal is (ReplI (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder ω Xi i U0) U HUtop).
An exact proof term for the current goal is (famunionI ω (λj : set ⇒ {product_cylinder ω Xi j U0|U0 ∈ space_family_topology Xi j}) i Cyl Hi HCylRepl).
We prove the intermediate claim HeqPre: preimage_of R_omega_space (Romega_coord_map i) U = Cyl.
Apply set_ext to the current goal.
Let f be given.
Assume HfPre: f ∈ preimage_of R_omega_space (Romega_coord_map i) U.
We will prove f ∈ Cyl.
We prove the intermediate claim HfX: f ∈ R_omega_space.
An exact proof term for the current goal is (SepE1 R_omega_space (λx0 : set ⇒ apply_fun (Romega_coord_map i) x0 ∈ U) f HfPre).
We prove the intermediate claim HfiU: apply_fun (Romega_coord_map i) f ∈ U.
An exact proof term for the current goal is (SepE2 R_omega_space (λx0 : set ⇒ apply_fun (Romega_coord_map i) x0 ∈ U) f HfPre).
We prove the intermediate claim Happ: apply_fun (Romega_coord_map i) f = apply_fun f i.
An exact proof term for the current goal is (Romega_coord_map_apply i f Hi HfX).
We prove the intermediate claim Hfprod: f ∈ product_space ω Xi.
rewrite the current goal using HXdef (from right to left).
An exact proof term for the current goal is HfX.
We prove the intermediate claim HfiU2: apply_fun f i ∈ U.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is HfiU.
We will prove f ∈ {g ∈ product_space ω Xi|i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U}.
Apply (SepI (product_space ω Xi) (λg : set ⇒ i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U) f Hfprod) to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hi.
An exact proof term for the current goal is HUtop.
An exact proof term for the current goal is HfiU2.
Let f be given.
Assume HfCyl: f ∈ Cyl.
We will prove f ∈ preimage_of R_omega_space (Romega_coord_map i) U.
We prove the intermediate claim Hfprod: f ∈ product_space ω Xi.
An exact proof term for the current goal is (SepE1 (product_space ω Xi) (λg : set ⇒ i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U) f HfCyl).
We prove the intermediate claim HfX: f ∈ R_omega_space.
rewrite the current goal using HXdef (from left to right).
An exact proof term for the current goal is Hfprod.
We prove the intermediate claim Hcond: i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U.
An exact proof term for the current goal is (SepE2 (product_space ω Xi) (λg : set ⇒ i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U) f HfCyl).
We prove the intermediate claim HfiU: apply_fun f i ∈ U.
An exact proof term for the current goal is (andER (i ∈ ω ∧ U ∈ space_family_topology Xi i) (apply_fun f i ∈ U) Hcond).
We prove the intermediate claim Happ: apply_fun (Romega_coord_map i) f = apply_fun f i.
An exact proof term for the current goal is (Romega_coord_map_apply i f Hi HfX).
We prove the intermediate claim Hpre_def: preimage_of R_omega_space (Romega_coord_map i) U = {x ∈ R_omega_space|apply_fun (Romega_coord_map i) x ∈ U}.
Use reflexivity.
rewrite the current goal using Hpre_def (from left to right).
Apply (SepI R_omega_space (λx0 : set ⇒ apply_fun (Romega_coord_map i) x0 ∈ U) f HfX) to the current goal.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is HfiU.
rewrite the current goal using HeqPre (from left to right).
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis R_omega_space S Cyl HS HCylS).
∎