We will prove topology_on R_omega_space R_omega_product_topology.
Set Xi to be the term const_space_family ω R R_standard_topology.
Set X to be the term product_space ω Xi.
Set S to be the term product_subbasis_full ω Xi.
Set Tx to be the term generated_topology_from_subbasis X S.
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim HcompTop: ∀i : set, i ∈ ω → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume Hi: i ∈ ω.
We will prove topology_on (space_family_set Xi i) (space_family_topology Xi 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 HTi: 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 HTi (from left to right).
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HSsub: S ⊆ 𝒫 X.
Let s be given.
Assume Hs: s ∈ S.
We will prove s ∈ 𝒫 X.
Apply PowerI to the current goal.
Let f be given.
Assume Hf: f ∈ s.
We will prove f ∈ X.
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) 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 ∈ X)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ space_family_topology Xi i.
Assume Hseq: s = product_cylinder ω Xi i U0.
We prove the intermediate claim HfCyl: f ∈ product_cylinder ω Xi i U0.
rewrite the current goal using Hseq (from right to left).
An exact proof term for the current goal is Hf.
An exact proof term for the current goal is (SepE1 X (λg0 : set ⇒ i ∈ ω ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun g0 i ∈ U0) f HfCyl).
We prove the intermediate claim HUnionS: ⋃ S = X.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ ⋃ S.
We will prove f ∈ X.
Apply UnionE_impred S f Hf to the current goal.
Let s be given.
Assume Hfs: f ∈ s.
Assume HsS: s ∈ S.
We prove the intermediate claim HsPow: s ∈ 𝒫 X.
An exact proof term for the current goal is (HSsub s HsS).
An exact proof term for the current goal is (PowerE X s HsPow f Hfs).
Let f be given.
Assume Hf: f ∈ X.
We will prove f ∈ ⋃ S.
Set i0 to be the term 0.
Set U0 to be the term space_family_set Xi i0.
Set s0 to be the term product_cylinder ω Xi i0 U0.
We prove the intermediate claim Hi0: i0 ∈ ω.
An exact proof term for the current goal is H0omega.
We prove the intermediate claim HTi0: topology_on (space_family_set Xi i0) (space_family_topology Xi i0).
An exact proof term for the current goal is (HcompTop i0 Hi0).
We prove the intermediate claim HU0top: U0 ∈ space_family_topology Xi i0.
An exact proof term for the current goal is (topology_has_X (space_family_set Xi i0) (space_family_topology Xi i0) HTi0).
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 Hs0Fi0: s0 ∈ F i0.
An exact proof term for the current goal is (ReplI (space_family_topology Xi i0) (λU : set ⇒ product_cylinder ω Xi i0 U) U0 HU0top).
An exact proof term for the current goal is (famunionI ω F i0 s0 Hi0 Hs0Fi0).
We will prove f ∈ ⋃ S.
Apply (UnionI S f s0) to the current goal.
We will prove f ∈ s0.
We will prove f ∈ {g ∈ X|i0 ∈ ω ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun g i0 ∈ U0}.
Apply (SepI X (λg0 : set ⇒ i0 ∈ ω ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun g0 i0 ∈ U0) f Hf) to the current goal.
We will prove i0 ∈ ω ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f i0 ∈ U0.
Apply andI to the current goal.
We will prove i0 ∈ ω ∧ U0 ∈ space_family_topology Xi i0.
Apply andI to the current goal.
An exact proof term for the current goal is Hi0.
An exact proof term for the current goal is HU0top.
We prove the intermediate claim Hfprop: total_function_on f ω (space_family_union ω Xi) ∧ functional_graph f ∧ ∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set Xi i.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω (space_family_union ω Xi))) (λf0 : set ⇒ total_function_on f0 ω (space_family_union ω Xi) ∧ functional_graph f0 ∧ ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set Xi i) f Hf).
We prove the intermediate claim Hcoords: ∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set Xi i.
An exact proof term for the current goal is (andER (total_function_on f ω (space_family_union ω Xi) ∧ functional_graph f) (∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set Xi i) Hfprop).
An exact proof term for the current goal is (Hcoords i0 Hi0).
An exact proof term for the current goal is Hs0S.
We prove the intermediate claim HS: subbasis_on X S.
We will prove S ⊆ 𝒫 X ∧ ⋃ S = X.
Apply andI to the current goal.
An exact proof term for the current goal is HSsub.
An exact proof term for the current goal is HUnionS.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (topology_from_subbasis_is_topology X S HS).
We prove the intermediate claim HXe: X = R_omega_space.
Use reflexivity.
We prove the intermediate claim HTXe: Tx = R_omega_product_topology.
Use reflexivity.
rewrite the current goal using HXe (from right to left).
rewrite the current goal using HTXe (from right to left).
An exact proof term for the current goal is HTx.
∎