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

• ex_network : ∃ (ι : Type) (f : ι → Set X), Countable ι ∧ IsKNetwork f