∀ {X : Type v} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] [T2Space X]
  {ι : X → Type u} {p : (x : X) → ι x → Prop} {B : (x : X) → ι x → Set X} {s : Set X},
  IsClosed s →
    (∀ x ∈ s, (nhds x).HasBasis (p x) (B x)) →
      ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ a, B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)