sum_apply' — Mathlib

English

For Countable ι, (Kernel.sum κ) a s = ∑' n, κ n a s.

Русский

Для счётного множества ι верна тождество: (Kernel.sum κ) a s = ∑' n, κ n a s.

LaTeX

$$$[Countable \\\\iota] \\\\Rightarrow \\\\text{Kernel.sum } κ \\\\ a \\\\ s = \\\\sum' n, κ n \\\\ a \\\\ s$$$

Lean4

theorem sum_apply' [Countable ι] (κ : ι → Kernel α β) (a : α) {s : Set β} (hs : MeasurableSet s) :
    Kernel.sum κ a s = ∑' n, κ n a s := by rw [sum_apply κ a, Measure.sum_apply _ hs]

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