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

• has_countable_network : ∃ (ι : Type) (f : ι → Set X), Countable ι ∧ IsNetwork f