We will prove ¬ connected_space (product_space ω (const_space_family ω R R_standard_topology)) (box_topology ω (const_space_family ω R R_standard_topology)).

Assume Hconn: connected_space R_omega_space R_omega_box_topology.

We will prove False.

We prove the intermediate claim Hnosep: ¬ (∃U V : set, U ∈ R_omega_box_topology ∧ V ∈ R_omega_box_topology ∧ separation_of R_omega_space U V).

An exact proof term for the current goal is (andER (topology_on R_omega_space R_omega_box_topology) (¬ (∃U V : set, U ∈ R_omega_box_topology ∧ V ∈ R_omega_box_topology ∧ separation_of R_omega_space U V)) Hconn).

We prove the intermediate claim Hsep: ∃U V : set, U ∈ R_omega_box_topology ∧ V ∈ R_omega_box_topology ∧ separation_of R_omega_space U V.

We use bounded_sequences_Romega to witness the existential quantifier.

We use unbounded_sequences_Romega to witness the existential quantifier.

Apply andI to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is bounded_sequences_in_Romega_box_topology.

An exact proof term for the current goal is unbounded_sequences_in_Romega_box_topology.

We will prove separation_of R_omega_space bounded_sequences_Romega unbounded_sequences_Romega.

Apply andI to the current goal.

Apply andI to the current goal.

Apply andI 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 bounded_sequences_Romega_in_Power.

An exact proof term for the current goal is unbounded_sequences_Romega_in_Power.

An exact proof term for the current goal is bounded_unbounded_disjoint_Romega.

An exact proof term for the current goal is bounded_sequences_Romega_nonempty.

An exact proof term for the current goal is unbounded_sequences_Romega_nonempty.

An exact proof term for the current goal is bounded_union_unbounded_Romega.

An exact proof term for the current goal is (Hnosep Hsep).

∎