Finite_Product_Space_is_Connected_iff_Factors_are_Connected_Basis_for_the_Induction
Provedconnectednessproduct-spacesproofwikitopology
A product of two topological spaces is connected iff both factors are connected.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Finite_Product_Space_is_Connected_iff_Factors_are_Connected_Basis_for_the_Induction {X Y : Type _} [TopologicalSpace X] [TopologicalSpace Y] : ConnectedSpace (X × Y) ↔ ConnectedSpace X ∧ ConnectedSpace Y := by sorrySource