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

• ex_basis : ∃ (ι : Type u) (f : ι → Set X), Sigma (fun {α : Type u} => LocallyFinite) f ∧ (∀ (i : ι), IsOpen (f i)) ∧ ∀ (x : X), ∀ s ∈ nhds x, ∃ (i : ι), x ∈ f i ∧ f i ⊆ s