We will prove connected_space (Romega_tilde 0) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde 0)).
Set X to be the term R_omega_space.
Set Tx to be the term R_omega_product_topology.
Set Y to be the term Romega_tilde 0.
Set Ty to be the term subspace_topology X Tx Y.
Set A to be the term image_of Romega_singleton_map R.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is Romega_product_topology_is_topology.
We prove the intermediate claim HYsub: Y ⊆ X.
An exact proof term for the current goal is (Romega_tilde_sub_Romega 0).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HYsub).
We prove the intermediate claim HAsubY: A ⊆ Y.
An exact proof term for the current goal is image_of_Romega_singleton_map_sub_Romega_tilde0.
We prove the intermediate claim HAconnX: connected_space A (subspace_topology X Tx A).
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 Hcont: continuous_map R R_standard_topology X Tx Romega_singleton_map.
An exact proof term for the current goal is Romega_singleton_map_continuous_prod.
An exact proof term for the current goal is (continuous_image_connected R R_standard_topology X Tx Romega_singleton_map HRconn Hcont).
We prove the intermediate claim HsubEq: subspace_topology Y Ty A = subspace_topology X Tx A.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx Y A HTx HYsub HAsubY).
We prove the intermediate claim HAconn: connected_space A (subspace_topology Y Ty A).
rewrite the current goal using HsubEq (from left to right).
An exact proof term for the current goal is HAconnX.
We prove the intermediate claim Hdense: closure_of Y Ty A = Y.
An exact proof term for the current goal is Romega_tilde0_singletons_dense_in_subspace.
An exact proof term for the current goal is (connected_space_if_dense_connected_subset Y Ty A HTy HAsubY HAconn Hdense).
∎