class PiBase.CozeroComplementedSpace (X : Type u_1) [TopologicalSpace X] : Prop

• cozero_complemented (s : Set X) : IsCozero s → ∃ (t : Set X), IsCozero t ∧ Disjoint s t ∧ Dense (s ∪ t)