English
If f is locally finite and each f_i is closed, then for any x, the intersection of the complements of f_i over indices with x not in f_i forms a neighborhood of x.
Русский
Если {f_i} локально конечна, и каждый f_i замкнуто, то для любой точки x пересечение дополнений f_i по тем индексам, где x ∉ f_i, образует окрестность x.
LaTeX
$$(⋂ (i) (_ : x ∉ f i), (f i)ᶜ) ∈ 𝓝 x$$
Lean4
/-- 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`. -/
theorem iInter_compl_mem_nhds (hf : LocallyFinite f) (hc : ∀ i, IsClosed (f i)) (x : X) :
(⋂ (i) (_ : x ∉ f i), (f i)ᶜ) ∈ 𝓝 x :=
by
refine IsOpen.mem_nhds ?_ (mem_iInter₂.2 fun i => id)
suffices IsClosed (⋃ i : { i // x ∉ f i }, f i) by rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this
exact (hf.comp_injective Subtype.val_injective).isClosed_iUnion fun i => hc _
