sum_coe_finset — Mathlib

English

For a finite set s of indices, the sum over s equals the Finset-sum: (sum i∈s μ_i) = ∑ i∈s μ_i.

Русский

Для конечного множества индексов s сумма по s равна конечной сумме по элементам: (sum i∈s μ_i) = ∑ i∈s μ_i.

LaTeX

$$$ (\sum i \in s, μ_i) = \sum_{i \in s} μ_i $$$

Lean4

theorem sum_coe_finset (s : Finset ι) (μ : ι → Measure α) : (sum fun i : s => μ i) = ∑ i ∈ s, μ i := by
  rw [sum_fintype, Finset.sum_coe_sort s μ]

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