Let k be given.
Assume HkO: k ∈ ω.
Set Dom to be the term setprod (Romega_tilde k) R.
Set Tx0 to be the term subspace_topology R_omega_space R_omega_product_topology (Romega_tilde k).
Set Tdom to be the term product_topology (Romega_tilde k) Tx0 R R_standard_topology.
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 HtopRomega: 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 HtopTildek: topology_on (Romega_tilde k) Tx0.
An exact proof term for the current goal is (subspace_topology_is_topology R_omega_space R_omega_product_topology (Romega_tilde k) HtopRomega (Romega_tilde_sub_Romega k)).
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 HtopDom: topology_on Dom Tdom.
An exact proof term for the current goal is (product_topology_is_topology (Romega_tilde k) Tx0 R R_standard_topology HtopTildek HtopR).
We prove the intermediate claim Hfun: function_on (Romega_extend_map k) Dom R_omega_space.
An exact proof term for the current goal is (Romega_extend_map_function_on k HkO).
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 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 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.
We prove the intermediate claim HSUnion: ⋃ S = R_omega_space.
Apply set_ext to the current goal.
Let f be given.
Assume HfU: f ∈ ⋃ S.
We will prove f ∈ R_omega_space.
Apply (UnionE_impred S f HfU) to the current goal.
Let s be given.
Assume Hfs: f ∈ s.
Assume HsS: s ∈ S.
We prove the intermediate claim HsPow: s ∈ 𝒫 R_omega_space.
An exact proof term for the current goal is (HSsubPow s HsS).
An exact proof term for the current goal is (PowerE R_omega_space s HsPow f Hfs).
Let f be given.
Assume HfX: f ∈ R_omega_space.
We will prove f ∈ ⋃ S.
Set s0 to be the term product_cylinder ω Xi 0 R.
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 HRin: R ∈ space_family_topology Xi 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).
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).
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 HfX 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 HfX.
We prove the intermediate claim Hfs0: f ∈ s0.
We prove the intermediate claim Hcyl_def: s0 = {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.
We prove the intermediate claim Hs0In: s0 ∈ {product_cylinder ω Xi 0 U0|U0 ∈ space_family_topology Xi 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).
We prove the intermediate claim Hs0S: s0 ∈ S.
An exact proof term for the current goal is (famunionI ω (λj : set ⇒ {product_cylinder ω Xi j U0|U0 ∈ space_family_topology Xi j}) 0 s0 H0o Hs0In).
An exact proof term for the current goal is (UnionI S f s0 Hfs0 Hs0S).
An exact proof term for the current goal is (andI (S ⊆ 𝒫 R_omega_space) (⋃ S = R_omega_space) HSsubPow HSUnion).
We prove the intermediate claim Hpre: ∀s : set, s ∈ S → preimage_of Dom (Romega_extend_map k) s ∈ Tdom.
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 Dom (Romega_extend_map k) s ∈ Tdom)) 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 Dom (Romega_extend_map k) s ∈ Tdom)) 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 (ordsucc k ∈ i)) to the current goal.
Assume HkLt: ordsucc k ∈ i.
Apply (xm (0 ∈ U)) to the current goal.
Assume H0U: 0 ∈ U.
We prove the intermediate claim Heq: preimage_of Dom (Romega_extend_map k) (product_cylinder ω Xi i U) = Dom.
Apply set_ext to the current goal.
Let p be given.
Assume HpPre: p ∈ preimage_of Dom (Romega_extend_map k) (product_cylinder ω Xi i U).
We will prove p ∈ Dom.
An exact proof term for the current goal is (SepE1 Dom (λp0 : set ⇒ apply_fun (Romega_extend_map k) p0 ∈ product_cylinder ω Xi i U) p HpPre).
Let p be given.
Assume Hp: p ∈ Dom.
We will prove p ∈ preimage_of Dom (Romega_extend_map k) (product_cylinder ω Xi i U).
We prove the intermediate claim Hpre_def: preimage_of Dom (Romega_extend_map k) (product_cylinder ω Xi i U) = {p0 ∈ Dom|apply_fun (Romega_extend_map k) p0 ∈ product_cylinder ω Xi i U}.
Use reflexivity.
rewrite the current goal using Hpre_def (from left to right).
Apply (SepI Dom (λp0 : set ⇒ apply_fun (Romega_extend_map k) p0 ∈ product_cylinder ω Xi i U) p Hp) to the current goal.
We prove the intermediate claim Himg: apply_fun (Romega_extend_map k) p ∈ R_omega_space.
An exact proof term for the current goal is (Romega_extend_map_function_on k HkO p Hp).
We prove the intermediate claim HXdef: R_omega_space = product_space ω Xi.
Use reflexivity.
We prove the intermediate claim HimgProd: apply_fun (Romega_extend_map k) p ∈ product_space ω Xi.
rewrite the current goal using HXdef (from right to left).
An exact proof term for the current goal is Himg.
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) (apply_fun (Romega_extend_map k) p) HimgProd) 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 Happmap: apply_fun (Romega_extend_map k) p = Romega_extend_seq k p.
rewrite the current goal using (Romega_extend_map_apply k p HkO Hp) (from left to right).
Use reflexivity.
rewrite the current goal using Happmap (from left to right).
Set h to be the term (λj : set ⇒ If_i (ordsucc k ∈ j) 0 (If_i (j = ordsucc k) (p 1) (apply_fun (p 0) j))).
We prove the intermediate claim HdefSeq: Romega_extend_seq k p = graph ω h.
Use reflexivity.
rewrite the current goal using HdefSeq (from left to right).
We prove the intermediate claim Happi: apply_fun (graph ω h) i = h i.
An exact proof term for the current goal is (apply_fun_graph ω h i Hi).
rewrite the current goal using Happi (from left to right).
We prove the intermediate claim Hhi: h i = If_i (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)).
Use reflexivity.
rewrite the current goal using Hhi (from left to right).
rewrite the current goal using (If_i_1 (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)) HkLt) (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 Dom Tdom HtopDom).
Assume Hn0U: ¬ (0 ∈ U).
We prove the intermediate claim Heq: preimage_of Dom (Romega_extend_map k) (product_cylinder ω Xi i U) = Empty.
Apply set_ext to the current goal.
Let p be given.
Assume HpPre: p ∈ preimage_of Dom (Romega_extend_map k) (product_cylinder ω Xi i U).
We will prove p ∈ Empty.
We prove the intermediate claim HpDom: p ∈ Dom.
An exact proof term for the current goal is (SepE1 Dom (λp0 : set ⇒ apply_fun (Romega_extend_map k) p0 ∈ product_cylinder ω Xi i U) p HpPre).
We prove the intermediate claim Hcond: apply_fun (Romega_extend_map k) p ∈ product_cylinder ω Xi i U.
An exact proof term for the current goal is (SepE2 Dom (λp0 : set ⇒ apply_fun (Romega_extend_map k) p0 ∈ product_cylinder ω Xi i U) p HpPre).
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 Hcond2: apply_fun (Romega_extend_map k) p ∈ {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 Hcond.
We prove the intermediate claim Hprop: i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun (apply_fun (Romega_extend_map k) p) 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) (apply_fun (Romega_extend_map k) p) Hcond2).
We prove the intermediate claim HUi: apply_fun (apply_fun (Romega_extend_map k) p) i ∈ U.
An exact proof term for the current goal is (andER (i ∈ ω ∧ U ∈ space_family_topology Xi i) (apply_fun (apply_fun (Romega_extend_map k) p) i ∈ U) Hprop).
We prove the intermediate claim Happmap: apply_fun (Romega_extend_map k) p = Romega_extend_seq k p.
rewrite the current goal using (Romega_extend_map_apply k p HkO HpDom) (from left to right).
Use reflexivity.
We prove the intermediate claim HUiSeq: apply_fun (Romega_extend_seq k p) i ∈ U.
rewrite the current goal using Happmap (from right to left).
An exact proof term for the current goal is HUi.
Set h to be the term (λj : set ⇒ If_i (ordsucc k ∈ j) 0 (If_i (j = ordsucc k) (p 1) (apply_fun (p 0) j))).
We prove the intermediate claim HdefSeq: Romega_extend_seq k p = graph ω h.
Use reflexivity.
We prove the intermediate claim HUiGraph: apply_fun (graph ω h) i ∈ U.
rewrite the current goal using HdefSeq (from right to left).
An exact proof term for the current goal is HUiSeq.
We prove the intermediate claim Happi: apply_fun (graph ω h) i = h i.
An exact proof term for the current goal is (apply_fun_graph ω h i Hi).
We prove the intermediate claim HH: h i ∈ U.
rewrite the current goal using Happi (from right to left).
An exact proof term for the current goal is HUiGraph.
We prove the intermediate claim Hhi: h i = If_i (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)).
Use reflexivity.
We prove the intermediate claim H0inU: 0 ∈ U.
rewrite the current goal using (If_i_1 (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)) HkLt) (from right to left).
rewrite the current goal using Hhi (from right to left).
An exact proof term for the current goal is HH.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hn0U H0inU).
Let p be given.
Assume Hp: p ∈ Empty.
We will prove p ∈ preimage_of Dom (Romega_extend_map k) (product_cylinder ω Xi i U).
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE p Hp).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_has_empty Dom Tdom HtopDom).
Assume HnKlt: ¬ (ordsucc k ∈ i).
Apply (xm (i = ordsucc k)) to the current goal.
Assume Hieq: i = ordsucc k.
We prove the intermediate claim Hproj2Cont: continuous_map Dom Tdom R R_standard_topology (projection2 (Romega_tilde k) R).
An exact proof term for the current goal is (projection2_continuous_in_product (Romega_tilde k) Tx0 R R_standard_topology HtopTildek HtopR).
We prove the intermediate claim HpreProj: preimage_of Dom (projection2 (Romega_tilde k) R) U ∈ Tdom.
An exact proof term for the current goal is (continuous_map_preimage Dom Tdom R R_standard_topology (projection2 (Romega_tilde k) R) Hproj2Cont U HUstd).
We prove the intermediate claim Heq: preimage_of Dom (Romega_extend_map k) (product_cylinder ω Xi i U) = preimage_of Dom (projection2 (Romega_tilde k) R) U.
Apply set_ext to the current goal.
Let p be given.
Assume HpPre: p ∈ preimage_of Dom (Romega_extend_map k) (product_cylinder ω Xi i U).
We will prove p ∈ preimage_of Dom (projection2 (Romega_tilde k) R) U.
We prove the intermediate claim HpDom: p ∈ Dom.
An exact proof term for the current goal is (SepE1 Dom (λp0 : set ⇒ apply_fun (Romega_extend_map k) p0 ∈ product_cylinder ω Xi i U) p HpPre).
We prove the intermediate claim Hcond: apply_fun (Romega_extend_map k) p ∈ product_cylinder ω Xi i U.
An exact proof term for the current goal is (SepE2 Dom (λp0 : set ⇒ apply_fun (Romega_extend_map k) p0 ∈ product_cylinder ω Xi i U) p HpPre).
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 Hcond2: apply_fun (Romega_extend_map k) p ∈ {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 Hcond.
We prove the intermediate claim Hprop: i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun (apply_fun (Romega_extend_map k) p) 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) (apply_fun (Romega_extend_map k) p) Hcond2).
We prove the intermediate claim HUi: apply_fun (apply_fun (Romega_extend_map k) p) i ∈ U.
An exact proof term for the current goal is (andER (i ∈ ω ∧ U ∈ space_family_topology Xi i) (apply_fun (apply_fun (Romega_extend_map k) p) i ∈ U) Hprop).
We prove the intermediate claim Happmap: apply_fun (Romega_extend_map k) p = Romega_extend_seq k p.
rewrite the current goal using (Romega_extend_map_apply k p HkO HpDom) (from left to right).
Use reflexivity.
We prove the intermediate claim HUiSeq: apply_fun (Romega_extend_seq k p) i ∈ U.
rewrite the current goal using Happmap (from right to left).
An exact proof term for the current goal is HUi.
Set h to be the term (λj : set ⇒ If_i (ordsucc k ∈ j) 0 (If_i (j = ordsucc k) (p 1) (apply_fun (p 0) j))).
We prove the intermediate claim HdefSeq: Romega_extend_seq k p = graph ω h.
Use reflexivity.
We prove the intermediate claim HUiGraph: apply_fun (graph ω h) i ∈ U.
rewrite the current goal using HdefSeq (from right to left).
An exact proof term for the current goal is HUiSeq.
We prove the intermediate claim Happi: apply_fun (graph ω h) i = h i.
An exact proof term for the current goal is (apply_fun_graph ω h i Hi).
We prove the intermediate claim HH: h i ∈ U.
rewrite the current goal using Happi (from right to left).
An exact proof term for the current goal is HUiGraph.
We prove the intermediate claim Hhi: h i = If_i (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)).
Use reflexivity.
We prove the intermediate claim Hp1U: p 1 ∈ U.
We prove the intermediate claim Hexpr: If_i (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)) ∈ U.
rewrite the current goal using Hhi (from right to left).
An exact proof term for the current goal is HH.
We prove the intermediate claim Hexpr2: If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i) ∈ U.
rewrite the current goal using (If_i_0 (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)) HnKlt) (from right to left).
An exact proof term for the current goal is Hexpr.
rewrite the current goal using (If_i_1 (i = ordsucc k) (p 1) (apply_fun (p 0) i) Hieq) (from right to left).
An exact proof term for the current goal is Hexpr2.
We prove the intermediate claim Hpre_def: preimage_of Dom (projection2 (Romega_tilde k) R) U = {p0 ∈ Dom|apply_fun (projection2 (Romega_tilde k) R) p0 ∈ U}.
Use reflexivity.
rewrite the current goal using Hpre_def (from left to right).
Apply (SepI Dom (λp0 : set ⇒ apply_fun (projection2 (Romega_tilde k) R) p0 ∈ U) p HpDom) to the current goal.
We prove the intermediate claim Happ2: apply_fun (projection2 (Romega_tilde k) R) p = p 1.
An exact proof term for the current goal is (projection2_apply (Romega_tilde k) R p HpDom).
rewrite the current goal using Happ2 (from left to right).
An exact proof term for the current goal is Hp1U.
Let p be given.
Assume HpPre: p ∈ preimage_of Dom (projection2 (Romega_tilde k) R) U.
We will prove p ∈ preimage_of Dom (Romega_extend_map k) (product_cylinder ω Xi i U).
We prove the intermediate claim HpDom: p ∈ Dom.
An exact proof term for the current goal is (SepE1 Dom (λp0 : set ⇒ apply_fun (projection2 (Romega_tilde k) R) p0 ∈ U) p HpPre).
We prove the intermediate claim HpU: apply_fun (projection2 (Romega_tilde k) R) p ∈ U.
An exact proof term for the current goal is (SepE2 Dom (λp0 : set ⇒ apply_fun (projection2 (Romega_tilde k) R) p0 ∈ U) p HpPre).
We prove the intermediate claim Happ2: apply_fun (projection2 (Romega_tilde k) R) p = p 1.
An exact proof term for the current goal is (projection2_apply (Romega_tilde k) R p HpDom).
We prove the intermediate claim Hp1U: p 1 ∈ U.
rewrite the current goal using Happ2 (from right to left).
An exact proof term for the current goal is HpU.
We prove the intermediate claim Hpre_def: preimage_of Dom (Romega_extend_map k) (product_cylinder ω Xi i U) = {p0 ∈ Dom|apply_fun (Romega_extend_map k) p0 ∈ product_cylinder ω Xi i U}.
Use reflexivity.
rewrite the current goal using Hpre_def (from left to right).
Apply (SepI Dom (λp0 : set ⇒ apply_fun (Romega_extend_map k) p0 ∈ product_cylinder ω Xi i U) p HpDom) to the current goal.
We prove the intermediate claim Himg: apply_fun (Romega_extend_map k) p ∈ R_omega_space.
An exact proof term for the current goal is (Romega_extend_map_function_on k HkO p HpDom).
We prove the intermediate claim HXdef: R_omega_space = product_space ω Xi.
Use reflexivity.
We prove the intermediate claim HimgProd: apply_fun (Romega_extend_map k) p ∈ product_space ω Xi.
rewrite the current goal using HXdef (from right to left).
An exact proof term for the current goal is Himg.
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) (apply_fun (Romega_extend_map k) p) HimgProd) 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 Happmap: apply_fun (Romega_extend_map k) p = Romega_extend_seq k p.
rewrite the current goal using (Romega_extend_map_apply k p HkO HpDom) (from left to right).
Use reflexivity.
rewrite the current goal using Happmap (from left to right).
Set h to be the term (λj : set ⇒ If_i (ordsucc k ∈ j) 0 (If_i (j = ordsucc k) (p 1) (apply_fun (p 0) j))).
We prove the intermediate claim HdefSeq: Romega_extend_seq k p = graph ω h.
Use reflexivity.
rewrite the current goal using HdefSeq (from left to right).
We prove the intermediate claim Happi: apply_fun (graph ω h) i = h i.
An exact proof term for the current goal is (apply_fun_graph ω h i Hi).
rewrite the current goal using Happi (from left to right).
We prove the intermediate claim Hhi: h i = If_i (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)).
Use reflexivity.
rewrite the current goal using Hhi (from left to right).
rewrite the current goal using (If_i_0 (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)) HnKlt) (from left to right).
rewrite the current goal using (If_i_1 (i = ordsucc k) (p 1) (apply_fun (p 0) i) Hieq) (from left to right).
An exact proof term for the current goal is Hp1U.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HpreProj.
Assume Hineq: ¬ (i = ordsucc k).
Set Cyl to be the term product_cylinder ω Xi i U.
We prove the intermediate claim HCylOpen: Cyl ∈ R_omega_product_topology.
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 (subbasis_elem_open_in_generated_from_subbasis R_omega_space S Cyl HS (famunionI ω (λj : set ⇒ {product_cylinder ω Xi j U0|U0 ∈ space_family_topology Xi j}) i Cyl Hi (ReplI (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder ω Xi i U0) U HUtop))).
Set A to be the term Cyl ∩ Romega_tilde k.
We prove the intermediate claim HAopen: A ∈ Tx0.
An exact proof term for the current goal is (subspace_topologyI R_omega_space R_omega_product_topology (Romega_tilde k) Cyl HCylOpen).
We prove the intermediate claim HAsub: A ⊆ Romega_tilde k.
An exact proof term for the current goal is (binintersect_Subq_2 Cyl (Romega_tilde k)).
We prove the intermediate claim Hproj1Cont: continuous_map Dom Tdom (Romega_tilde k) Tx0 (projection1 (Romega_tilde k) R).
An exact proof term for the current goal is (projection1_continuous_in_product (Romega_tilde k) Tx0 R R_standard_topology HtopTildek HtopR).
We prove the intermediate claim HpreProj: preimage_of Dom (projection1 (Romega_tilde k) R) A ∈ Tdom.
An exact proof term for the current goal is (continuous_map_preimage Dom Tdom (Romega_tilde k) Tx0 (projection1 (Romega_tilde k) R) Hproj1Cont A HAopen).
We prove the intermediate claim Heq: preimage_of Dom (Romega_extend_map k) Cyl = preimage_of Dom (projection1 (Romega_tilde k) R) A.
Apply set_ext to the current goal.
Let p be given.
Assume HpPre: p ∈ preimage_of Dom (Romega_extend_map k) Cyl.
We will prove p ∈ preimage_of Dom (projection1 (Romega_tilde k) R) A.
We prove the intermediate claim HpDom: p ∈ Dom.
An exact proof term for the current goal is (SepE1 Dom (λp0 : set ⇒ apply_fun (Romega_extend_map k) p0 ∈ Cyl) p HpPre).
We prove the intermediate claim Hcond: apply_fun (Romega_extend_map k) p ∈ Cyl.
An exact proof term for the current goal is (SepE2 Dom (λp0 : set ⇒ apply_fun (Romega_extend_map k) p0 ∈ Cyl) p HpPre).
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.
We prove the intermediate claim Hcond2: apply_fun (Romega_extend_map k) p ∈ {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 Hcond.
We prove the intermediate claim Hprop: i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun (apply_fun (Romega_extend_map k) p) 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) (apply_fun (Romega_extend_map k) p) Hcond2).
We prove the intermediate claim HUi: apply_fun (apply_fun (Romega_extend_map k) p) i ∈ U.
An exact proof term for the current goal is (andER (i ∈ ω ∧ U ∈ space_family_topology Xi i) (apply_fun (apply_fun (Romega_extend_map k) p) i ∈ U) Hprop).
We prove the intermediate claim Happmap: apply_fun (Romega_extend_map k) p = Romega_extend_seq k p.
rewrite the current goal using (Romega_extend_map_apply k p HkO HpDom) (from left to right).
Use reflexivity.
We prove the intermediate claim HUiSeq: apply_fun (Romega_extend_seq k p) i ∈ U.
rewrite the current goal using Happmap (from right to left).
An exact proof term for the current goal is HUi.
Set h to be the term (λj : set ⇒ If_i (ordsucc k ∈ j) 0 (If_i (j = ordsucc k) (p 1) (apply_fun (p 0) j))).
We prove the intermediate claim HdefSeq: Romega_extend_seq k p = graph ω h.
Use reflexivity.
We prove the intermediate claim HUiGraph: apply_fun (graph ω h) i ∈ U.
rewrite the current goal using HdefSeq (from right to left).
An exact proof term for the current goal is HUiSeq.
We prove the intermediate claim Happi: apply_fun (graph ω h) i = h i.
An exact proof term for the current goal is (apply_fun_graph ω h i Hi).
We prove the intermediate claim HH: h i ∈ U.
rewrite the current goal using Happi (from right to left).
An exact proof term for the current goal is HUiGraph.
We prove the intermediate claim Hhi: h i = If_i (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)).
Use reflexivity.
We prove the intermediate claim Hp0iU: apply_fun (p 0) i ∈ U.
rewrite the current goal using (If_i_0 (i = ordsucc k) (p 1) (apply_fun (p 0) i) Hineq) (from right to left).
rewrite the current goal using (If_i_0 (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)) HnKlt) (from right to left).
rewrite the current goal using Hhi (from right to left).
An exact proof term for the current goal is HH.
We prove the intermediate claim Hp0: apply_fun (projection1 (Romega_tilde k) R) p = p 0.
An exact proof term for the current goal is (projection1_apply (Romega_tilde k) R p HpDom).
We prove the intermediate claim Hp0In: p 0 ∈ A.
We prove the intermediate claim Hp0Tilde: p 0 ∈ Romega_tilde k.
An exact proof term for the current goal is (ap0_Sigma (Romega_tilde k) (λ_ : set ⇒ R) p HpDom).
We prove the intermediate claim Hp0Cyl: p 0 ∈ Cyl.
We prove the intermediate claim HXdef: R_omega_space = product_space ω Xi.
Use reflexivity.
We prove the intermediate claim Hp0Romega: p 0 ∈ R_omega_space.
An exact proof term for the current goal is (Romega_tilde_sub_Romega k (p 0) Hp0Tilde).
We prove the intermediate claim Hp0Prod: p 0 ∈ product_space ω Xi.
rewrite the current goal using HXdef (from right to left).
An exact proof term for the current goal is Hp0Romega.
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) (p 0) Hp0Prod) 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 Hp0iU.
An exact proof term for the current goal is (binintersectI Cyl (Romega_tilde k) (p 0) Hp0Cyl Hp0Tilde).
We prove the intermediate claim Hpre_def: preimage_of Dom (projection1 (Romega_tilde k) R) A = {p0 ∈ Dom|apply_fun (projection1 (Romega_tilde k) R) p0 ∈ A}.
Use reflexivity.
rewrite the current goal using Hpre_def (from left to right).
Apply (SepI Dom (λp0 : set ⇒ apply_fun (projection1 (Romega_tilde k) R) p0 ∈ A) p HpDom) to the current goal.
rewrite the current goal using Hp0 (from left to right).
An exact proof term for the current goal is Hp0In.
Let p be given.
Assume HpPre: p ∈ preimage_of Dom (projection1 (Romega_tilde k) R) A.
We will prove p ∈ preimage_of Dom (Romega_extend_map k) Cyl.
We prove the intermediate claim HpDom: p ∈ Dom.
An exact proof term for the current goal is (SepE1 Dom (λp0 : set ⇒ apply_fun (projection1 (Romega_tilde k) R) p0 ∈ A) p HpPre).
We prove the intermediate claim HpA: apply_fun (projection1 (Romega_tilde k) R) p ∈ A.
An exact proof term for the current goal is (SepE2 Dom (λp0 : set ⇒ apply_fun (projection1 (Romega_tilde k) R) p0 ∈ A) p HpPre).
We prove the intermediate claim Hp0: apply_fun (projection1 (Romega_tilde k) R) p = p 0.
An exact proof term for the current goal is (projection1_apply (Romega_tilde k) R p HpDom).
We prove the intermediate claim Hp0A: p 0 ∈ A.
rewrite the current goal using Hp0 (from right to left).
An exact proof term for the current goal is HpA.
We prove the intermediate claim Hp0Cyl: p 0 ∈ Cyl.
An exact proof term for the current goal is (binintersectE1 Cyl (Romega_tilde k) (p 0) Hp0A).
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.
We prove the intermediate claim Hprop0: i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun (p 0) i ∈ U.
We prove the intermediate claim Hp0Cyl2: p 0 ∈ {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 Hp0Cyl.
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) (p 0) Hp0Cyl2).
We prove the intermediate claim HUi0: apply_fun (p 0) i ∈ U.
An exact proof term for the current goal is (andER (i ∈ ω ∧ U ∈ space_family_topology Xi i) (apply_fun (p 0) i ∈ U) Hprop0).
We prove the intermediate claim Hpre_def: preimage_of Dom (Romega_extend_map k) Cyl = {p0 ∈ Dom|apply_fun (Romega_extend_map k) p0 ∈ Cyl}.
Use reflexivity.
rewrite the current goal using Hpre_def (from left to right).
Apply (SepI Dom (λp0 : set ⇒ apply_fun (Romega_extend_map k) p0 ∈ Cyl) p HpDom) to the current goal.
We prove the intermediate claim Himg: apply_fun (Romega_extend_map k) p ∈ R_omega_space.
An exact proof term for the current goal is (Romega_extend_map_function_on k HkO p HpDom).
We prove the intermediate claim HXdef: R_omega_space = product_space ω Xi.
Use reflexivity.
We prove the intermediate claim HimgProd: apply_fun (Romega_extend_map k) p ∈ product_space ω Xi.
rewrite the current goal using HXdef (from right to left).
An exact proof term for the current goal is Himg.
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) (apply_fun (Romega_extend_map k) p) HimgProd) 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 Happmap: apply_fun (Romega_extend_map k) p = Romega_extend_seq k p.
rewrite the current goal using (Romega_extend_map_apply k p HkO HpDom) (from left to right).
Use reflexivity.
rewrite the current goal using Happmap (from left to right).
Set h to be the term (λj : set ⇒ If_i (ordsucc k ∈ j) 0 (If_i (j = ordsucc k) (p 1) (apply_fun (p 0) j))).
We prove the intermediate claim HdefSeq: Romega_extend_seq k p = graph ω h.
Use reflexivity.
rewrite the current goal using HdefSeq (from left to right).
We prove the intermediate claim Happi: apply_fun (graph ω h) i = h i.
An exact proof term for the current goal is (apply_fun_graph ω h i Hi).
rewrite the current goal using Happi (from left to right).
We prove the intermediate claim Hhi: h i = If_i (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)).
Use reflexivity.
rewrite the current goal using Hhi (from left to right).
rewrite the current goal using (If_i_0 (ordsucc k ∈ i) 0 (If_i (i = ordsucc k) (p 1) (apply_fun (p 0) i)) HnKlt) (from left to right).
rewrite the current goal using (If_i_0 (i = ordsucc k) (p 1) (apply_fun (p 0) i) Hineq) (from left to right).
An exact proof term for the current goal is HUi0.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HpreProj.
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 Dom Tdom R_omega_space S (Romega_extend_map k) HtopDom Hfun HS Hpre).
∎