Let n be given.
Assume HnO: n ∈ ω.
Set X to be the term R_omega_space.
Set Tx to be the term R_omega_product_topology.
We will prove connected_space (Romega_tilde n) (subspace_topology X Tx (Romega_tilde n)).
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
Apply (nat_ind (λk : set ⇒ connected_space (Romega_tilde k) (subspace_topology X Tx (Romega_tilde k)))) to the current goal.
An exact proof term for the current goal is Romega_tilde0_connected.
Let k be given.
Assume HkNat: nat_p k.
Assume IHk: connected_space (Romega_tilde k) (subspace_topology X Tx (Romega_tilde k)).
We will prove connected_space (Romega_tilde (ordsucc k)) (subspace_topology X Tx (Romega_tilde (ordsucc k))).
We prove the intermediate claim HkO: k ∈ ω.
An exact proof term for the current goal is (nat_p_omega k HkNat).
We prove the intermediate claim HRconn: connected_space R R_standard_topology.
An exact proof term for the current goal is interval_connected.
We prove the intermediate claim Hprod: connected_space (setprod (Romega_tilde k) R) (product_topology (Romega_tilde k) (subspace_topology X Tx (Romega_tilde k)) R R_standard_topology).
An exact proof term for the current goal is (finite_product_connected (Romega_tilde k) (subspace_topology X Tx (Romega_tilde k)) R R_standard_topology IHk HRconn).
We prove the intermediate claim Hhom: homeomorphism (setprod (Romega_tilde k) R) (product_topology (Romega_tilde k) (subspace_topology X Tx (Romega_tilde k)) R R_standard_topology) (Romega_tilde (ordsucc k)) (subspace_topology X Tx (Romega_tilde (ordsucc k))) (Romega_extend_map k).
An exact proof term for the current goal is (Romega_tilde_succ_homeomorphism k HkO).
An exact proof term for the current goal is (homeomorphism_preserves_connected (setprod (Romega_tilde k) R) (product_topology (Romega_tilde k) (subspace_topology X Tx (Romega_tilde k)) R R_standard_topology) (Romega_tilde (ordsucc k)) (subspace_topology X Tx (Romega_tilde (ordsucc k))) (Romega_extend_map k) Hhom Hprod).
An exact proof term for the current goal is HnNat.
∎