We will prove connected_space Romega_infty (subspace_topology R_omega_space R_omega_box_topology Romega_infty).
Set X to be the term R_omega_space.
Set Tx to be the term R_omega_box_topology.
Set F to be the term {Romega_tilde n|n ∈ ω}.
We prove the intermediate claim HTx: topology_on X Tx.
We prove the intermediate claim HXeq: X = product_space ω (const_space_family ω R R_standard_topology).
Use reflexivity.
We prove the intermediate claim HTxeq: Tx = box_topology ω (const_space_family ω R R_standard_topology).
Use reflexivity.
rewrite the current goal using HXeq (from left to right).
rewrite the current goal using HTxeq (from left to right).
Apply (box_topology_is_topology_on ω (const_space_family ω R R_standard_topology)) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
We will prove topology_on (space_family_set (const_space_family ω R R_standard_topology) i) (space_family_topology (const_space_family ω R R_standard_topology) i).
rewrite the current goal using (space_family_set_const_space_family ω R R_standard_topology i Hi) (from left to right).
rewrite the current goal using (space_family_topology_const_space_family ω R R_standard_topology i Hi) (from left to right).
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HFsub: ∀C : set, C ∈ F → C ⊆ X.
Let C be given.
Assume HC: C ∈ F.
We will prove C ⊆ X.
Apply (ReplE_impred ω (λn : set ⇒ Romega_tilde n) C HC (C ⊆ X)) to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume HCeq: C = Romega_tilde n.
rewrite the current goal using HCeq (from left to right).
An exact proof term for the current goal is (Romega_tilde_sub_Romega n).
We prove the intermediate claim HFconn: ∀C : set, C ∈ F → connected_space C (subspace_topology X Tx C).
Let C be given.
Assume HC: C ∈ F.
We will prove connected_space C (subspace_topology X Tx C).
Apply (ReplE_impred ω (λn : set ⇒ Romega_tilde n) C HC (connected_space C (subspace_topology X Tx C))) to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume HCeq: C = Romega_tilde n.
rewrite the current goal using HCeq (from left to right).
An exact proof term for the current goal is (Romega_tilde_connected_box n Hn).
We prove the intermediate claim Hcommon: ∃x : set, ∀C : set, C ∈ F → x ∈ C.
We use Romega_zero to witness the existential quantifier.
Let C be given.
Assume HC: C ∈ F.
We will prove Romega_zero ∈ C.
Apply (ReplE_impred ω (λn : set ⇒ Romega_tilde n) C HC (Romega_zero ∈ C)) to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume HCeq: C = Romega_tilde n.
rewrite the current goal using HCeq (from left to right).
An exact proof term for the current goal is (Romega_zero_in_Romega_tilde n Hn).
We prove the intermediate claim HconnUnion: connected_space (⋃ F) (subspace_topology X Tx (⋃ F)).
An exact proof term for the current goal is (union_connected_common_point X Tx F HTx HFsub HFconn Hcommon).
We prove the intermediate claim HUnionEq: ⋃ F = Romega_infty.
Use reflexivity.
rewrite the current goal using HUnionEq (from left to right).
rewrite the current goal using HUnionEq (from left to right) at position 1.
An exact proof term for the current goal is HconnUnion.
∎