English
Let s be a locally finite family of subsets of X indexed by ι, with each s_i closed. For any x ∈ X, there exists a neighborhood of x such that for every y in that neighborhood, the set of indices i with y ∈ s_i is contained in the set of indices with x ∈ s_i.
Русский
Пусть {s_i} — локально конечное семейство подмножеств X с индексами i ∈ ι, каждый s_i замкнуто. Для любого x ∈ X найдется окрестность U(x), такая что для все y ∈ U(x) множество индексов i с y ∈ s_i содержится в множество индексов с x ∈ s_i.
LaTeX
$$$\\forall x \\in X, \\exists U \\in \\mathcal{N}(x), \\forall y \\in U, \\{i \\mid y \\in s_i\\} \\subseteq \\{i \\mid x \\in s_i\\}$$$
Lean4
theorem eventually_subset {s : ι → Set X} (hs : LocallyFinite s) (hs' : ∀ i, IsClosed (s i)) (x : X) :
∀ᶠ y in 𝓝 x, {i | y ∈ s i} ⊆ {i | x ∈ s i} :=
by
filter_upwards [hs.iInter_compl_mem_nhds hs' x] with y hy i hi
simp only [mem_iInter, mem_compl_iff] at hy
exact not_imp_not.mp (hy i) hi
