Theorems · Theorem · general topology

LocallyFinite.iInter_compl_mem_nhds

∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
  LocallyFinite f → (∀ (i : ι), IsClosed (f i)) → ∀ (x : X), ⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ ∈ nhds x

If f : β → Set α is a locally finite family of closed sets, then for any x : α, the intersection of the complements to f i, x ∉ f i, is a neighbourhood of x.

Defined in

Mathlib.Topology.LocallyFinite

Cited by

2 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace