English
Let α and β be topological spaces that are totally disconnected. Then α × β is totally disconnected.
Русский
Пусть пространства α и β являются полностью раздельными; тогда произведение α × β также полностью раздельно.
LaTeX
$$$TotallyDisconnectedSpace(\alpha) \land TotallyDisconnectedSpace(\beta) \Rightarrow TotallyDisconnectedSpace(\alpha \times \beta)$$$
Lean4
instance totallyDisconnectedSpace [TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] :
TotallyDisconnectedSpace (α × β) :=
⟨fun t _ h2 =>
have H1 : IsPreconnected (Prod.fst '' t) := h2.image Prod.fst continuous_fst.continuousOn
have H2 : IsPreconnected (Prod.snd '' t) := h2.image Prod.snd continuous_snd.continuousOn
fun x hx y hy => Prod.ext (H1.subsingleton ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩) (H2.subsingleton ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩)⟩
