prodMkRight_add — Mathlib

English

Sum over a countable index of prodMkLeft γ (κ_i) equals prodMkLeft γ (Sum_i κ_i); i.e., Kernel.sum (i ↦ prodMkLeft γ (κ_i)) = prodMkLeft γ (Kernel.sum κ).

Русский

Сумма по счётному индексу от prodMkLeft γ (κ_i) равна prodMkLeft γ (сумма κ_i).

LaTeX

$$$ \operatorname{sum} i \bigl( \operatorname{prodMkLeft} γ (κ_i) \bigr) = \operatorname{prodMkLeft} γ (\operatorname{sum} i κ_i )$$$

Lean4

@[simp]
theorem prodMkRight_add (κ η : Kernel α β) : prodMkRight γ (κ + η) = prodMkRight γ κ + prodMkRight γ η := by ext; simp

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