English
The dependent sum Σ_i X_i is totally disconnected if every fiber X_i is totally disconnected.
Русский
Зависимая сумма Σ_i X_i полностью раздельна, если каждый X_i полностью раздельен.
LaTeX
$$$(\\forall i, TotallyDisconnectedSpace(X_i)) \Rightarrow TotallyDisconnectedSpace(\\Sigma i, X_i)$$$
Lean4
instance [∀ i, TopologicalSpace (X i)] [∀ i, TotallyDisconnectedSpace (X i)] : TotallyDisconnectedSpace (Σ i, X i) :=
by
refine ⟨fun s _ hs => ?_⟩
obtain rfl | h := s.eq_empty_or_nonempty
· exact subsingleton_empty
· obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩
exact ht.isPreconnected.subsingleton.image _