English
Let ρ be a partition of unity on X indexed by ι, and x0 ∈ X. Then there exists a finite subset I ⊆ ι and a neighborhood N of x0 such that for every x ∈ N, the finite sum ∑_{i∈I} ρ_i(x) equals 1 and the support of the vector x ↦ (ρ_i(x))_{i∈ι} lies inside I.
Русский
Пусть ρ — это разбиение единиц на X индексируемое по ι. Пусть x0 ∈ X. Тогда существует конечное подмножество I ⊆ ι и окрестность N(x0) such что для каждого x ∈ N выполняется ∑_{i∈I} ρ_i(x) = 1 и поддержка вектора x ↦ (ρ_i(x))_{i∈ι} ⊆ I.
LaTeX
$$$$\exists I \subseteq ι,\ I \text{ finite},\ \exists N \in \mathcal{N}(x_0),\ N \subseteq X:\quad \forall x \in N,\ \sum_{i \in I} ρ_i(x) = 1 \ \wedge\ \mathrm{supp}(ρ(\cdot, x)) \subseteq I.$$$$
Lean4
theorem exists_finset_nhds (ρ : PartitionOfUnity ι X univ) (x₀ : X) :
∃ I : Finset ι, ∀ᶠ x in 𝓝 x₀, ∑ i ∈ I, ρ i x = 1 ∧ support (ρ · x) ⊆ I :=
by
rcases ρ.exists_finset_nhds' x₀ with ⟨I, H⟩
use I
rwa [nhdsWithin_univ, ← eventually_and] at H
