English
There exists a finite index set I such that within nhds x0 (relative to s), the sum over I equals 1, and near x0 the support of ρ·x is contained in I.
Русский
Существует конечный набор индексов I, для которого в окружности nhds x0 ∩ s сумма по I равна 1, и около x0 поддержка ρ·x ⊆ I.
LaTeX
$$$\exists I: Finset ι, (∀ x \in nhdsWithin x_0 s, \sum_{i∈I} ρ(i)(x) = 1) ∧ (∀ x \in nhds x_0, \operatorname{support}(ρ·x) ⊆ I)$$$
Lean4
theorem exists_finset_nhds' {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) :
∃ I : Finset ι, (∀ᶠ x in 𝓝[s] x₀, ∑ i ∈ I, ρ i x = 1) ∧ ∀ᶠ x in 𝓝 x₀, support (ρ · x) ⊆ I :=
by
rcases ρ.locallyFinite.exists_finset_support x₀ with ⟨I, hI⟩
refine ⟨I, eventually_nhdsWithin_iff.mpr (hI.mono fun x hx x_in ↦ ?_), hI⟩
have : ∑ᶠ i : ι, ρ i x = ∑ i ∈ I, ρ i x := finsum_eq_sum_of_support_subset _ hx
rwa [eq_comm, ρ.sum_eq_one x_in] at this
