We will prove continuous_map R R_standard_topology R_omega_space R_omega_product_topology Romega_singleton_map.
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 HtopR: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim Hfun: function_on Romega_singleton_map R R_omega_space.
An exact proof term for the current goal is Romega_singleton_map_function_on.
We prove the intermediate claim Hone: ω ≠ 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 Hcomp: ∀i : set, i ∈ ω → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume Hi: i ∈ ω.
We prove the intermediate claim HXi: 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 Hset: space_family_set Xi i = R.
We prove the intermediate claim Hdef: space_family_set Xi i = (apply_fun Xi i) 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 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 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.
We prove the intermediate claim HS: subbasis_on R_omega_space S.
We will prove S ⊆ 𝒫 R_omega_space ∧ ⋃ S = R_omega_space.
Apply andI to the current goal.
Let s be given.
Assume Hs: s ∈ S.
We will prove s ∈ 𝒫 R_omega_space.
Apply PowerI to the current goal.
Let f be given.
Assume Hf: f ∈ s.
We will prove f ∈ R_omega_space.
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 (f ∈ R_omega_space)) 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 (f ∈ R_omega_space)) to the current goal.
Let U be given.
Assume HU: U ∈ space_family_topology Xi i.
Assume Hseq: s = product_cylinder ω Xi i U.
We prove the intermediate claim HfCyl: f ∈ product_cylinder ω Xi i U.
rewrite the current goal using Hseq (from right to left).
An exact proof term for the current goal is Hf.
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).
An exact proof term for the current goal is Hfprod.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ ⋃ S.
We will prove f ∈ R_omega_space.
We prove the intermediate claim HSsubPow: S ⊆ 𝒫 R_omega_space.
Let s be given.
Assume Hs: s ∈ S.
We will prove s ∈ 𝒫 R_omega_space.
Apply PowerI to the current goal.
Let g be given.
Assume Hg: g ∈ s.
We will prove g ∈ R_omega_space.
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 (g ∈ R_omega_space)) 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 (g ∈ R_omega_space)) to the current goal.
Let U be given.
Assume HU: U ∈ space_family_topology Xi i.
Assume Hseq: s = product_cylinder ω Xi i U.
We prove the intermediate claim HgCyl: g ∈ product_cylinder ω Xi i U.
rewrite the current goal using Hseq (from right to left).
An exact proof term for the current goal is Hg.
An exact proof term for the current goal is (SepE1 (product_space ω Xi) (λh : set ⇒ i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun h i ∈ U) g HgCyl).
Apply (UnionE_impred S f Hf) to the current goal.
Let s be given.
Assume Hfs: f ∈ s.
Assume Hs: s ∈ S.
We prove the intermediate claim HsPow: s ∈ 𝒫 R_omega_space.
An exact proof term for the current goal is (HSsubPow s Hs).
We prove the intermediate claim HsSub: s ⊆ R_omega_space.
An exact proof term for the current goal is (PowerE R_omega_space s HsPow).
An exact proof term for the current goal is (HsSub f Hfs).
Let f be given.
Assume Hf: f ∈ R_omega_space.
We will prove f ∈ ⋃ S.
We prove the intermediate claim H0o: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim HXi0: apply_fun Xi 0 = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology 0 H0o).
We prove the intermediate claim Htop0: space_family_topology Xi 0 = R_standard_topology.
We prove the intermediate claim Hdef: space_family_topology Xi 0 = (apply_fun Xi 0) 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 HRin: R ∈ space_family_topology Xi 0.
rewrite the current goal using Htop0 (from left to right).
An exact proof term for the current goal is (topology_has_X R R_standard_topology R_standard_topology_is_topology).
Set s0 to be the term product_cylinder ω Xi 0 R.
We prove the intermediate claim Hs0S: s0 ∈ S.
Set F to be the term (λi : set ⇒ {product_cylinder ω Xi i U|U ∈ space_family_topology Xi i}).
We prove the intermediate claim Hs0F0: s0 ∈ F 0.
An exact proof term for the current goal is (ReplI (space_family_topology Xi 0) (λU0 : set ⇒ product_cylinder ω Xi 0 U0) R HRin).
An exact proof term for the current goal is (famunionI ω F 0 s0 H0o Hs0F0).
We prove the intermediate claim Hf0R: apply_fun f 0 ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R f 0 Hf H0o).
We prove the intermediate claim HXdef: R_omega_space = product_space ω Xi.
Use reflexivity.
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 Hf.
We prove the intermediate claim Hfs0: f ∈ s0.
We prove the intermediate claim Hs0def: s0 = product_cylinder ω Xi 0 R.
Use reflexivity.
rewrite the current goal using Hs0def (from left to right).
We prove the intermediate claim Hcyl_def: product_cylinder ω Xi 0 R = {g ∈ product_space ω Xi|0 ∈ ω ∧ R ∈ space_family_topology Xi 0 ∧ apply_fun g 0 ∈ R}.
Use reflexivity.
rewrite the current goal using Hcyl_def (from left to right).
Apply (SepI (product_space ω Xi) (λg : set ⇒ 0 ∈ ω ∧ R ∈ space_family_topology Xi 0 ∧ apply_fun g 0 ∈ R) 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 H0o.
An exact proof term for the current goal is HRin.
An exact proof term for the current goal is Hf0R.
An exact proof term for the current goal is (UnionI S f s0 Hfs0 Hs0S).
We prove the intermediate claim Hpre: ∀s : set, s ∈ S → preimage_of R Romega_singleton_map s ∈ R_standard_topology.
Let s be given.
Assume Hs: s ∈ S.
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 Romega_singleton_map s ∈ R_standard_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 Romega_singleton_map s ∈ R_standard_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 HXi: 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 HXi (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.
We prove the intermediate claim HUsubR: U ⊆ R.
We prove the intermediate claim HtopSub: R_standard_topology ⊆ 𝒫 R.
An exact proof term for the current goal is (topology_subset_axiom R R_standard_topology R_standard_topology_is_topology).
We prove the intermediate claim HUpow: U ∈ 𝒫 R.
An exact proof term for the current goal is (HtopSub U HUstd).
An exact proof term for the current goal is (PowerE R U HUpow).
Apply (xm (0 ∈ i)) to the current goal.
Assume H0i: 0 ∈ i.
Apply (xm (0 ∈ U)) to the current goal.
Assume H0U: 0 ∈ U.
We prove the intermediate claim Heq: preimage_of R Romega_singleton_map (product_cylinder ω Xi i U) = R.
Apply set_ext to the current goal.
Let r be given.
Assume Hrpre: r ∈ preimage_of R Romega_singleton_map (product_cylinder ω Xi i U).
We will prove r ∈ R.
We prove the intermediate claim Hrpre2: r ∈ {x0 ∈ R|apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U}.
We prove the intermediate claim Hpre_def: preimage_of R Romega_singleton_map (product_cylinder ω Xi i U) = {x0 ∈ R|apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U}.
Use reflexivity.
rewrite the current goal using Hpre_def (from right to left).
An exact proof term for the current goal is Hrpre.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U) r Hrpre2).
Let r be given.
Assume HrR: r ∈ R.
We will prove r ∈ preimage_of R Romega_singleton_map (product_cylinder ω Xi i U).
We prove the intermediate claim Hpre_def: preimage_of R Romega_singleton_map (product_cylinder ω Xi i U) = {x0 ∈ R|apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U}.
Use reflexivity.
rewrite the current goal using Hpre_def (from left to right).
Apply (SepI R (λx0 : set ⇒ apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U) r HrR) to the current goal.
We will prove apply_fun Romega_singleton_map r ∈ product_cylinder ω Xi i U.
We prove the intermediate claim Happmap: apply_fun Romega_singleton_map r = Romega_singleton_seq r.
An exact proof term for the current goal is (Romega_singleton_map_apply r HrR).
rewrite the current goal using Happmap (from left to right).
We prove the intermediate claim HXdef: R_omega_space = product_space ω Xi.
Use reflexivity.
We prove the intermediate claim Hrseq: Romega_singleton_seq r ∈ product_space ω Xi.
rewrite the current goal using HXdef (from right to left).
An exact proof term for the current goal is (Romega_singleton_seq_in_Romega_space r HrR).
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_singleton_seq r) Hrseq) 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 Happi: apply_fun (Romega_singleton_seq r) i = If_i (0 ∈ i) 0 r.
An exact proof term for the current goal is (Romega_singleton_seq_apply r i HrR Hi).
rewrite the current goal using Happi (from left to right).
rewrite the current goal using (If_i_1 (0 ∈ i) 0 r H0i) (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 R_standard_topology R_standard_topology_is_topology).
Assume Hn0U: ¬ (0 ∈ U).
We prove the intermediate claim Heq: preimage_of R Romega_singleton_map (product_cylinder ω Xi i U) = Empty.
Apply set_ext to the current goal.
Let r be given.
Assume Hrpre: r ∈ preimage_of R Romega_singleton_map (product_cylinder ω Xi i U).
We will prove r ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim Hrpre2: r ∈ {x0 ∈ R|apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U}.
We prove the intermediate claim Hpre_def: preimage_of R Romega_singleton_map (product_cylinder ω Xi i U) = {x0 ∈ R|apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U}.
Use reflexivity.
rewrite the current goal using Hpre_def (from right to left).
An exact proof term for the current goal is Hrpre.
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U) r Hrpre2).
We prove the intermediate claim Hcond: apply_fun Romega_singleton_map r ∈ product_cylinder ω Xi i U.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U) r Hrpre2).
We prove the intermediate claim Happmap: apply_fun Romega_singleton_map r = Romega_singleton_seq r.
An exact proof term for the current goal is (Romega_singleton_map_apply r HrR).
We prove the intermediate claim Hcond2: Romega_singleton_seq r ∈ product_cylinder ω Xi i U.
rewrite the current goal using Happmap (from right to left).
An exact proof term for the current goal is Hcond.
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.
We prove the intermediate claim Hcond3: Romega_singleton_seq r ∈ {g ∈ product_space ω Xi|i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U}.
rewrite the current goal using Hcyl_def (from right to left).
An exact proof term for the current goal is Hcond2.
We prove the intermediate claim Hprop: i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun (Romega_singleton_seq r) 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_singleton_seq r) Hcond3).
We prove the intermediate claim Hri: apply_fun (Romega_singleton_seq r) i ∈ U.
An exact proof term for the current goal is (andER (i ∈ ω ∧ U ∈ space_family_topology Xi i) (apply_fun (Romega_singleton_seq r) i ∈ U) Hprop).
We prove the intermediate claim Happi: apply_fun (Romega_singleton_seq r) i = If_i (0 ∈ i) 0 r.
An exact proof term for the current goal is (Romega_singleton_seq_apply r i HrR Hi).
We prove the intermediate claim HriIf: If_i (0 ∈ i) 0 r ∈ U.
rewrite the current goal using Happi (from right to left).
An exact proof term for the current goal is Hri.
We prove the intermediate claim Hif1: If_i (0 ∈ i) 0 r = 0.
An exact proof term for the current goal is (If_i_1 (0 ∈ i) 0 r H0i).
We prove the intermediate claim H0U: 0 ∈ U.
rewrite the current goal using Hif1 (from right to left).
An exact proof term for the current goal is HriIf.
An exact proof term for the current goal is (Hn0U H0U).
Let r be given.
Assume HrE: r ∈ Empty.
We will prove r ∈ preimage_of R Romega_singleton_map (product_cylinder ω Xi i U).
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE r HrE).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_has_empty R R_standard_topology R_standard_topology_is_topology).
Assume Hn0i: ¬ (0 ∈ i).
We prove the intermediate claim Heq: preimage_of R Romega_singleton_map (product_cylinder ω Xi i U) = U.
Apply set_ext to the current goal.
Let r be given.
Assume Hrpre: r ∈ preimage_of R Romega_singleton_map (product_cylinder ω Xi i U).
We will prove r ∈ U.
We prove the intermediate claim Hrpre2: r ∈ {x0 ∈ R|apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U}.
We prove the intermediate claim Hpre_def: preimage_of R Romega_singleton_map (product_cylinder ω Xi i U) = {x0 ∈ R|apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U}.
Use reflexivity.
rewrite the current goal using Hpre_def (from right to left).
An exact proof term for the current goal is Hrpre.
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U) r Hrpre2).
We prove the intermediate claim Hcond: apply_fun Romega_singleton_map r ∈ product_cylinder ω Xi i U.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U) r Hrpre2).
We prove the intermediate claim Happmap: apply_fun Romega_singleton_map r = Romega_singleton_seq r.
An exact proof term for the current goal is (Romega_singleton_map_apply r HrR).
We prove the intermediate claim Hcond2: Romega_singleton_seq r ∈ product_cylinder ω Xi i U.
rewrite the current goal using Happmap (from right to left).
An exact proof term for the current goal is Hcond.
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.
We prove the intermediate claim Hcond3: Romega_singleton_seq r ∈ {g ∈ product_space ω Xi|i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U}.
rewrite the current goal using Hcyl_def (from right to left).
An exact proof term for the current goal is Hcond2.
We prove the intermediate claim Hprop: i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun (Romega_singleton_seq r) 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_singleton_seq r) Hcond3).
We prove the intermediate claim Hri: apply_fun (Romega_singleton_seq r) i ∈ U.
An exact proof term for the current goal is (andER (i ∈ ω ∧ U ∈ space_family_topology Xi i) (apply_fun (Romega_singleton_seq r) i ∈ U) Hprop).
We prove the intermediate claim Happi: apply_fun (Romega_singleton_seq r) i = If_i (0 ∈ i) 0 r.
An exact proof term for the current goal is (Romega_singleton_seq_apply r i HrR Hi).
We prove the intermediate claim HriIf: If_i (0 ∈ i) 0 r ∈ U.
rewrite the current goal using Happi (from right to left).
An exact proof term for the current goal is Hri.
We prove the intermediate claim Hif0: If_i (0 ∈ i) 0 r = r.
An exact proof term for the current goal is (If_i_0 (0 ∈ i) 0 r Hn0i).
rewrite the current goal using Hif0 (from right to left).
An exact proof term for the current goal is HriIf.
Let r be given.
Assume HrU: r ∈ U.
We will prove r ∈ preimage_of R Romega_singleton_map (product_cylinder ω Xi i U).
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (HUsubR r HrU).
We prove the intermediate claim Hpre_def: preimage_of R Romega_singleton_map (product_cylinder ω Xi i U) = {x0 ∈ R|apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U}.
Use reflexivity.
rewrite the current goal using Hpre_def (from left to right).
Apply (SepI R (λx0 : set ⇒ apply_fun Romega_singleton_map x0 ∈ product_cylinder ω Xi i U) r HrR) to the current goal.
We will prove apply_fun Romega_singleton_map r ∈ product_cylinder ω Xi i U.
We prove the intermediate claim Happmap: apply_fun Romega_singleton_map r = Romega_singleton_seq r.
An exact proof term for the current goal is (Romega_singleton_map_apply r HrR).
rewrite the current goal using Happmap (from left to right).
We prove the intermediate claim HXdef: R_omega_space = product_space ω Xi.
Use reflexivity.
We prove the intermediate claim Hrseq: Romega_singleton_seq r ∈ product_space ω Xi.
rewrite the current goal using HXdef (from right to left).
An exact proof term for the current goal is (Romega_singleton_seq_in_Romega_space r HrR).
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_singleton_seq r) Hrseq) 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 Happi: apply_fun (Romega_singleton_seq r) i = If_i (0 ∈ i) 0 r.
An exact proof term for the current goal is (Romega_singleton_seq_apply r i HrR Hi).
rewrite the current goal using Happi (from left to right).
rewrite the current goal using (If_i_0 (0 ∈ i) 0 r Hn0i) (from left to right).
An exact proof term for the current goal is HrU.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HUstd.
We prove the intermediate claim HdefTy: R_omega_product_topology = generated_topology_from_subbasis R_omega_space S.
Use reflexivity.
rewrite the current goal using HdefTy (from left to right).
An exact proof term for the current goal is (continuous_map_from_subbasis R R_standard_topology R_omega_space S Romega_singleton_map HtopR Hfun HS Hpre).
∎