sum_fintype — Mathlib

English

If ι is a finite type, then the sum equals the finite sum over all i in the universe: sum μ = ∑ i μ_i.

Русский

Если индексное множество ι конечно, то сумма равна конечной сумме по всем i: sum μ = ∑ i μ_i.

LaTeX

$$$ [\text{Fintype } ι] \; (\sum μ) = \sum_i μ_i $$$

Lean4

@[simp]
theorem sum_fintype [Fintype ι] (μ : ι → Measure α) : sum μ = ∑ i, μ i :=
  by
  ext1 s hs
  simp only [sum_apply, finset_sum_apply, hs, tsum_fintype]

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