Let k be given.
Assume HkO: k ∈ ω.
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 Hfun: function_on (Romega_restrict_map k) R_omega_space R_omega_space.
An exact proof term for the current goal is (Romega_restrict_map_function_on k HkO).
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.
Apply (continuous_map_from_subbasis R_omega_space R_omega_product_topology R_omega_space S (Romega_restrict_map k) HtopX Hfun HS) to the current goal.
Let s be given.
Assume Hs: s ∈ S.
We will prove preimage_of R_omega_space (Romega_restrict_map k) s ∈ R_omega_product_topology.
Set F to be the term (λi : set ⇒ {product_cylinder ω Xi i U|U ∈ space_family_topology Xi i}).
We prove the intermediate claim HsF: s ∈ (⋃i ∈ ωF i).
An exact proof term for the current goal is Hs.
Apply (famunionE_impred ω F s HsF (preimage_of R_omega_space (Romega_restrict_map k) s ∈ R_omega_product_topology)) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
Assume HsFi: s ∈ F i.
Apply (ReplE_impred (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder ω Xi i U0) s HsFi (preimage_of R_omega_space (Romega_restrict_map k) s ∈ R_omega_product_topology)) to the current goal.
Let U be given.
Assume HUtop: U ∈ space_family_topology Xi i.
Assume Hseq: s = product_cylinder ω Xi i U.
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim Htopi: space_family_topology Xi i = R_standard_topology.
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 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).
We prove the intermediate claim HUstd: U ∈ R_standard_topology.
rewrite the current goal using Htopi (from right to left).
An exact proof term for the current goal is HUtop.
Apply (xm (k ∈ i)) to the current goal.
Assume Hki: k ∈ i.
Apply (xm (0 ∈ U)) to the current goal.
Assume H0U: 0 ∈ U.
We prove the intermediate claim Heq: preimage_of R_omega_space (Romega_restrict_map k) (product_cylinder ω Xi i U) = R_omega_space.
Apply set_ext to the current goal.
Let f be given.
Assume HfPre: f ∈ preimage_of R_omega_space (Romega_restrict_map k) (product_cylinder ω Xi i U).
An exact proof term for the current goal is (SepE1 R_omega_space (λx0 : set ⇒ apply_fun (Romega_restrict_map k) x0 ∈ product_cylinder ω Xi i U) f HfPre).
Let f be given.
Assume HfX: f ∈ R_omega_space.
We will prove f ∈ preimage_of R_omega_space (Romega_restrict_map k) (product_cylinder ω Xi i U).
We prove the intermediate claim Hpre_def: preimage_of R_omega_space (Romega_restrict_map k) (product_cylinder ω Xi i U) = {x ∈ R_omega_space|apply_fun (Romega_restrict_map k) x ∈ product_cylinder ω Xi i U}.
Use reflexivity.
rewrite the current goal using Hpre_def (from left to right).
Apply (SepI R_omega_space (λx0 : set ⇒ apply_fun (Romega_restrict_map k) x0 ∈ product_cylinder ω Xi i U) f HfX) to the current goal.
rewrite the current goal using (Romega_restrict_map_apply k f HkO HfX) (from left to right).
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 HimgTilde: Romega_restrict_seq k f ∈ Romega_tilde k.
An exact proof term for the current goal is (Romega_restrict_seq_in_Romega_tilde k f HkO HfX).
We prove the intermediate claim Himg: Romega_restrict_seq k f ∈ product_space ω Xi.
rewrite the current goal using HXdef (from right to left).
An exact proof term for the current goal is (Romega_tilde_sub_Romega k (Romega_restrict_seq k f) HimgTilde).
We will prove Romega_restrict_seq k f ∈ product_cylinder ω Xi i U.
We prove the intermediate claim Hcyl_def: product_cylinder ω Xi i U = {g ∈ product_space ω Xi|i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U}.
Use reflexivity.
rewrite the current goal using Hcyl_def (from left to right).
Apply (SepI (product_space ω Xi) (λg : set ⇒ i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U) (Romega_restrict_seq k f) Himg) 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.
We prove the intermediate claim Happ: apply_fun (Romega_restrict_seq k f) i = If_i (k ∈ i) 0 (apply_fun f i).
An exact proof term for the current goal is (Romega_restrict_seq_apply k f i HkO HfX Hi).
rewrite the current goal using Happ (from left to right).
rewrite the current goal using (If_i_1 (k ∈ i) 0 (apply_fun f i) Hki) (from left to right).
An exact proof term for the current goal is H0U.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_has_X R_omega_space R_omega_product_topology HtopX).
Assume Hn0U: ¬ (0 ∈ U).
We prove the intermediate claim Heq: preimage_of R_omega_space (Romega_restrict_map k) (product_cylinder ω Xi i U) = Empty.
Apply set_ext to the current goal.
Let f be given.
Assume HfPre: f ∈ preimage_of R_omega_space (Romega_restrict_map k) (product_cylinder ω Xi i U).
We will prove f ∈ Empty.
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_restrict_map k) x0 ∈ product_cylinder ω Xi i U) f HfPre).
We prove the intermediate claim Himg: apply_fun (Romega_restrict_map k) f ∈ product_cylinder ω Xi i U.
An exact proof term for the current goal is (SepE2 R_omega_space (λx0 : set ⇒ apply_fun (Romega_restrict_map k) x0 ∈ product_cylinder ω Xi i U) f HfPre).
We prove the intermediate claim Himg2: Romega_restrict_seq k f ∈ product_cylinder ω Xi i U.
rewrite the current goal using (Romega_restrict_map_apply k f HkO HfX) (from right to left).
An exact proof term for the current goal is Himg.
We prove the intermediate claim Hcond: i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun (Romega_restrict_seq k 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) (Romega_restrict_seq k f) Himg2).
We prove the intermediate claim HUi: apply_fun (Romega_restrict_seq k f) i ∈ U.
An exact proof term for the current goal is (andER (i ∈ ω ∧ U ∈ space_family_topology Xi i) (apply_fun (Romega_restrict_seq k f) i ∈ U) Hcond).
We prove the intermediate claim Happ: apply_fun (Romega_restrict_seq k f) i = If_i (k ∈ i) 0 (apply_fun f i).
An exact proof term for the current goal is (Romega_restrict_seq_apply k f i HkO HfX Hi).
Apply FalseE to the current goal.
We prove the intermediate claim Htmp: If_i (k ∈ i) 0 (apply_fun f i) ∈ U.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is HUi.
We prove the intermediate claim H0U2: 0 ∈ U.
rewrite the current goal using (If_i_1 (k ∈ i) 0 (apply_fun f i) Hki) (from right to left).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is (Hn0U H0U2).
Let f be given.
Assume HfE: f ∈ Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE f HfE).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HTx: topology_on R_omega_space R_omega_product_topology.
An exact proof term for the current goal is HtopX.
An exact proof term for the current goal is (topology_has_empty R_omega_space R_omega_product_topology HTx).
Assume Hnki: ¬ (k ∈ i).
Set Cyl to be the term product_cylinder ω Xi i U.
We prove the intermediate claim Heq: preimage_of R_omega_space (Romega_restrict_map k) Cyl = Cyl.
Apply set_ext to the current goal.
Let f be given.
Assume HfPre: f ∈ preimage_of R_omega_space (Romega_restrict_map k) Cyl.
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_restrict_map k) x0 ∈ Cyl) f HfPre).
We prove the intermediate claim Himg: apply_fun (Romega_restrict_map k) f ∈ Cyl.
An exact proof term for the current goal is (SepE2 R_omega_space (λx0 : set ⇒ apply_fun (Romega_restrict_map k) x0 ∈ Cyl) f HfPre).
We prove the intermediate claim Himg2: Romega_restrict_seq k f ∈ Cyl.
rewrite the current goal using (Romega_restrict_map_apply k f HkO HfX) (from right to left).
An exact proof term for the current goal is Himg.
We prove the intermediate claim Hcond: i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun (Romega_restrict_seq k 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) (Romega_restrict_seq k f) Himg2).
We prove the intermediate claim HUi: apply_fun (Romega_restrict_seq k f) i ∈ U.
An exact proof term for the current goal is (andER (i ∈ ω ∧ U ∈ space_family_topology Xi i) (apply_fun (Romega_restrict_seq k f) i ∈ U) Hcond).
We prove the intermediate claim Happ: apply_fun (Romega_restrict_seq k f) i = If_i (k ∈ i) 0 (apply_fun f i).
An exact proof term for the current goal is (Romega_restrict_seq_apply k f i HkO HfX Hi).
We prove the intermediate claim Htmp: If_i (k ∈ i) 0 (apply_fun f i) ∈ U.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is HUi.
We prove the intermediate claim HUi2: apply_fun f i ∈ U.
rewrite the current goal using (If_i_0 (k ∈ i) 0 (apply_fun f i) Hnki) (from right to left).
An exact proof term for the current goal is Htmp.
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 Hcyl_def: Cyl = {g ∈ product_space ω Xi|i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U}.
Use reflexivity.
rewrite the current goal using Hcyl_def (from left to right).
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 HUi2.
Let f be given.
Assume HfCyl: f ∈ Cyl.
We will prove f ∈ preimage_of R_omega_space (Romega_restrict_map k) Cyl.
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 HUi: apply_fun f i ∈ U.
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).
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 Hpre_def: preimage_of R_omega_space (Romega_restrict_map k) Cyl = {x ∈ R_omega_space|apply_fun (Romega_restrict_map k) x ∈ Cyl}.
Use reflexivity.
rewrite the current goal using Hpre_def (from left to right).
Apply (SepI R_omega_space (λx0 : set ⇒ apply_fun (Romega_restrict_map k) x0 ∈ Cyl) f HfX) to the current goal.
rewrite the current goal using (Romega_restrict_map_apply k f HkO HfX) (from left to right).
We prove the intermediate claim Himg: Romega_restrict_seq k f ∈ product_space ω Xi.
We prove the intermediate claim HimgTilde: Romega_restrict_seq k f ∈ Romega_tilde k.
An exact proof term for the current goal is (Romega_restrict_seq_in_Romega_tilde k f HkO HfX).
rewrite the current goal using HXdef (from right to left).
An exact proof term for the current goal is (Romega_tilde_sub_Romega k (Romega_restrict_seq k f) HimgTilde).
We prove the intermediate claim Hcyl_def2: Cyl = {g ∈ product_space ω Xi|i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U}.
Use reflexivity.
rewrite the current goal using Hcyl_def2 (from left to right).
Apply (SepI (product_space ω Xi) (λg : set ⇒ i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U) (Romega_restrict_seq k f) Himg) 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.
We prove the intermediate claim Happ: apply_fun (Romega_restrict_seq k f) i = If_i (k ∈ i) 0 (apply_fun f i).
An exact proof term for the current goal is (Romega_restrict_seq_apply k f i HkO HfX Hi).
rewrite the current goal using Happ (from left to right).
rewrite the current goal using (If_i_0 (k ∈ i) 0 (apply_fun f i) Hnki) (from left to right).
An exact proof term for the current goal is HUi.
rewrite the current goal using Heq (from left to right).
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).
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis R_omega_space S Cyl HS HCylS).
∎