comp_sum_right — Mathlib

English

If ι is a countable index set and κ: ι → Kernel α β, η: Kernel β γ, then composing η with Kernel.sum κ equals Kernel.sum of the compositions: η ∘ₖ Kernel.sum κ = Kernel.sum (i ↦ η ∘ₖ (κ i)).

Русский

Если индексное множество ι счётно и κ: ι → Kernel α β, η: Kernel β γ, то композиция η с суммой Kernel.sum κ равна сумме композиций: η ∘ₖ Kernel.sum κ = Kernel.sum (i ↦ η ∘ₖ κ i).

LaTeX

$$$ \eta \circ_K \Kernel.sum \kappa = \Kernel.sum (\lambda i. \eta \circ_K (\kappa i))$$$

Lean4

theorem comp_sum_right {ι : Type*} [Countable ι] (κ : ι → Kernel α β) (η : Kernel β γ) :
    η ∘ₖ Kernel.sum κ = Kernel.sum fun i ↦ η ∘ₖ (κ i) :=
  by
  ext _ _ hs
  simp_rw [sum_apply, comp_apply' _ _ _ hs, Measure.sum_apply _ hs, sum_apply, lintegral_sum_measure,
    comp_apply' _ _ _ hs]

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