sum_fintype — Mathlib

English

If ι is finite, Kernel.sum κ equals the finite sum ∑ i, κ i.

Русский

Если индекс ι конечен, сумма по Kernel равна конечному суммированию ∑ i, κ i.

LaTeX

$$$[Fintype \\\\iota] \\\\Rightarrow Kernel.sum κ = \\\\sum i, κ i$$$

Lean4

@[simp]
theorem sum_fintype [Fintype ι] (κ : ι → Kernel α β) : Kernel.sum κ = ∑ i, κ i :=
  by
  ext a s hs
  simp only [sum_apply' κ a hs, finset_sum_apply' _ κ a s, tsum_fintype]

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