English
Let f_i : X → M (with M a monoid with 1) be a family whose pointwise mulSupport is locally finite. Then for any x0 ∈ X there exists a finite subset I ⊆ ι such that in a neighborhood of x0, the indices i with f_i(x) ≠ 1 lie inside I.
Русский
Пусть дана семейство функций f_i : X → M, где M — моноид с единицей. Пусть множество поддержек по i, mulSupport(f_i), образует локально конечную семью. Тогда для любого x0 ∈ X существует конечный подмножество I ⊆ ι такое, что в окрестности x0 множества индексов с f_i(x) ≠ 1 лежат в I.
LaTeX
$$$\\exists I : \\mathrm{Finset}\\,\\iota,\\; \\forall^\\infty x \\in \\mathcal{N}(x_0),\\ (\\operatorname{mulSupport}(\\lambda i \\mapsto f_i(x))) \\subseteq I$$$
Lean4
@[to_additive]
theorem exists_finset_mulSupport {M : Type*} [One M] {f : ι → X → M} (hf : LocallyFinite fun i => mulSupport <| f i)
(x₀ : X) : ∃ I : Finset ι, ∀ᶠ x in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ I :=
by
rcases hf x₀ with ⟨U, hxU, hUf⟩
refine ⟨hUf.toFinset, mem_of_superset hxU fun y hy i hi => ?_⟩
rw [hUf.coe_toFinset]
exact ⟨y, hi, hy⟩
