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

• ex_network : ∃ (ι : Type u) (f : ι → Set X), Sigma (fun {α : Type u} => LocallyFinite) f ∧ IsNetwork f