instTotallyDisconnectedSpaceSigma

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 _

Похожие утверждения