class PiBase.SigmaConnectedSpace (X : Type u) [TopologicalSpace X] extends PreconnectedSpace X : Prop

• isPreconnected_univ : IsPreconnected Set.univ
• no_partition (f : ℕ → Set X) : Function.Injective f ∧ Setoid.IsPartition (Set.range f) → ∃ (n : ℕ), ¬IsClosed (f n)