sum_finsupport' — Mathlib

English

The finsum of i with weights ρ i x0 times φ i x0 equals the finsum over i of ρ i x0 · φ i x0.

Русский

Сумма по i веса ρ i x0 умноженных на φ i x0 равна finsum по i ρ i x0 · φ i x0.

LaTeX

$$$\sum i \in \rho.finsupport x_0, \rho i x_0 \cdot \phi i x_0 = \sum^\infty_i \rho i x_0 \cdot \phi i x_0$$$

Lean4

theorem sum_finsupport' (hx₀ : x₀ ∈ s) {I : Finset ι} (hI : ρ.finsupport x₀ ⊆ I) : ∑ i ∈ I, ρ i x₀ = 1 :=
  ρ.toPartitionOfUnity.sum_finsupport' hx₀ hI

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