fintsupport — Mathlib

English

For any φ, the finite sum with f_i(x0) multiplied by φ_i(x0) equals the finsum of f_i(x0) times φ_i(x0).

Русский

Для любого φ верна равенство конечной суммы над finsupport и бесконечной суммы с множителем φ.

LaTeX

$$$\sum_{i \in ρ.finsupport x_0} f_i(x_0) \cdot φ_i(x_0) = \sum_{i} f_i(x_0) \cdot φ_i(x_0)$$$

Lean4

/-- The tsupport of a partition of unity at a point `x₀` as a `Finset`.
  This is the set of `i : ι` such that `x₀ ∈ tsupport f i`. -/
def fintsupport (x₀ : X) : Finset ι :=
  (ρ.finite_tsupport x₀).toFinset

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