sum_zero — Mathlib

English

Sum of a countable family of zero kernels is the zero kernel.

Русский

Сумма счётной коллекции нулевых ядер есть нулевое ядро.

LaTeX

$$$[Countable \\\\iota] \\\\Rightarrow (Kernel.sum fun _ : \\\\iota => (0 : Kernel α β)) = 0$$$

Lean4

@[simp]
theorem sum_zero [Countable ι] : (Kernel.sum fun _ : ι => (0 : Kernel α β)) = 0 :=
  by
  ext a s hs
  rw [sum_apply' _ a hs]
  simp only [zero_apply, Measure.coe_zero, Pi.zero_apply, tsum_zero]

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