sum_finsupport — Mathlib

English

The correspondence ρ.finsupport x0 as a set equals the finite support transformed to a set.

Русский

Соответствие ρ.finsupport x0 как множество равно поддержке функции.

LaTeX

$$$ρ.finsupport x_0 = (ρ.finsupport x_0).toSet$$$

Lean4

theorem sum_finsupport (hx₀ : x₀ ∈ s) : ∑ i ∈ ρ.finsupport x₀, ρ i x₀ = 1 := by
  rw [← ρ.sum_eq_one hx₀, finsum_eq_sum_of_support_subset _ (ρ.coe_finsupport x₀).superset]

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