sum_prodMkLeft — Mathlib

English

For any countable index set, Kernel.sum of the left product kernels equals the left product of the sum kernel: Kernel.sum (i ↦ Kernel.prodMkLeft γ (κ_i)) = Kernel.prodMkLeft γ (Kernel.sum κ).

Русский

Для произвольной счетной множества индексов сумма левых произведений равна левому произведению от суммы ядер.

LaTeX

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

Lean4

theorem sum_prodMkLeft {ι : Type*} [Countable ι] {κ : ι → Kernel α β} :
    Kernel.sum (fun i ↦ Kernel.prodMkLeft γ (κ i)) = Kernel.prodMkLeft γ (Kernel.sum κ) :=
  by
  ext
  simp_rw [sum_apply, prodMkLeft_apply, sum_apply]

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