We will prove closure_of R_omega_space R_omega_product_topology Romega_infty = R_omega_space.
Apply set_ext to the current goal.
An exact proof term for the current goal is (closure_in_space R_omega_space R_omega_product_topology Romega_infty Romega_product_topology_is_topology).
Let x be given.
Assume Hx: x ∈ R_omega_space.
We will prove x ∈ closure_of R_omega_space R_omega_product_topology Romega_infty.
We prove the intermediate claim Hcond: ∀U : set, U ∈ R_omega_product_topology → x ∈ U → U ∩ Romega_infty ≠ Empty.
Let U be given.
Assume HU: U ∈ R_omega_product_topology.
Assume HxU: x ∈ U.
We will prove U ∩ Romega_infty ≠ Empty.
Set S to be the term product_subbasis_full ω (const_space_family ω R R_standard_topology).
Set B to be the term basis_of_subbasis R_omega_space S.
We prove the intermediate claim HUpow: U ∈ 𝒫 R_omega_space.
An exact proof term for the current goal is (SepE1 (𝒫 R_omega_space) (λU0 : set ⇒ ∀y ∈ U0, ∃b0 ∈ B, y ∈ b0 ∧ b0 ⊆ U0) U HU).
We prove the intermediate claim HUl: ∀y ∈ U, ∃b0 ∈ B, y ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R_omega_space) (λU0 : set ⇒ ∀y ∈ U0, ∃b0 ∈ B, y ∈ b0 ∧ b0 ⊆ U0) U HU).
Apply (HUl x HxU) to the current goal.
Let b0 be given.
Assume Hb0pair.
We prove the intermediate claim Hb0B: b0 ∈ B.
An exact proof term for the current goal is (andEL (b0 ∈ B) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hb0xu: x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (andER (b0 ∈ B) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hxb0: x ∈ b0.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ U) Hb0xu).
We prove the intermediate claim Hb0subU: b0 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ U) Hb0xu).
We prove the intermediate claim Hb0neA: b0 ∩ Romega_infty ≠ Empty.
An exact proof term for the current goal is (Romega_infty_meets_product_basis b0 x Hb0B Hxb0).
Assume HUAempty: U ∩ Romega_infty = Empty.
We prove the intermediate claim Hb0A_sub: b0 ∩ Romega_infty ⊆ U ∩ Romega_infty.
Let y be given.
Assume Hy: y ∈ b0 ∩ Romega_infty.
We prove the intermediate claim Hyb0: y ∈ b0.
An exact proof term for the current goal is (binintersectE1 b0 Romega_infty y Hy).
We prove the intermediate claim HyA: y ∈ Romega_infty.
An exact proof term for the current goal is (binintersectE2 b0 Romega_infty y Hy).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (Hb0subU y Hyb0).
An exact proof term for the current goal is (binintersectI U Romega_infty y HyU HyA).
We prove the intermediate claim Hb0A_empty: b0 ∩ Romega_infty = Empty.
Apply Empty_Subq_eq to the current goal.
We prove the intermediate claim HUAE: U ∩ Romega_infty ⊆ Empty.
Let y be given.
Assume Hy: y ∈ U ∩ Romega_infty.
We will prove y ∈ Empty.
rewrite the current goal using HUAempty (from right to left).
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is (Subq_tra (b0 ∩ Romega_infty) (U ∩ Romega_infty) Empty Hb0A_sub HUAE).
An exact proof term for the current goal is (Hb0neA Hb0A_empty).
An exact proof term for the current goal is (SepI R_omega_space (λx0 ⇒ ∀U : set, U ∈ R_omega_product_topology → x0 ∈ U → U ∩ Romega_infty ≠ Empty) x Hx Hcond).
∎