∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] (b : ι → Set X),
  TopologicalSpace.IsTopologicalBasis (Set.range b) →
    (∀ (i : ι), IsLindelof (b i)) → ∀ (U : Set X), IsLindelof U ∧ IsOpen U ↔ ∃ s, s.Countable ∧ U = ⋃ i ∈ s, b i