class PiBase.WeaklyLindelofSpace (X : Type u) [TopologicalSpace X] : Prop

• weakly_lindelof {ι : Type u} (U : ι → Set X) : (∀ (i : ι), IsOpen (U i)) → ⋃ (i : ι), U i = Set.univ → ∃ (t : Set ι), t.Countable ∧ Dense (⋃ i ∈ t, U i)