class PiBase.BiconnectedSpace (X : Type u_1) [TopologicalSpace X] extends PreconnectedSpace X : Prop

• isPreconnected_univ : IsPreconnected Set.univ
• no_partition (s v : Set X) : ConnectedSpace ↑s → s.Nontrivial → ConnectedSpace ↑v → v.Nontrivial → (s ∩ v).Nonempty