mem_fintsupport_iff — Mathlib

English

There exists a finite index set I such that, locally near x0 within s, the sum over I equals 1, and near x0 the supports are contained in I.

Русский

Существует конечный набор индексов I, для которого в окрестности x0 внутри s сумма по I даёт 1, и окрестности указывает что поддержка лежит в I.

LaTeX

$$$\exists I:\ Finset ι, (∀^{x}_{nhds[s] x_0}, \sum_{i∈I} ρ_i(x) = 1) ∧ (∀^{x}_{nhds x_0}, \operatorname{support}(ρ·x) ⊆ I)$$$

Lean4

theorem mem_fintsupport_iff (i : ι) : i ∈ ρ.fintsupport x₀ ↔ x₀ ∈ tsupport (ρ i) :=
  Finite.mem_toFinset _

Похожие утверждения