comp_add_left — Mathlib

English

Let μ be a kernel α → β and κ, η be kernels β → γ. Then (κ + η) ∘ₖ μ = κ ∘ₖ μ + η ∘ₖ μ.

Русский

Пусть μ: α → β, κ, η: β → γ. Тогда композиция (κ + η) с μ равна сумме композиций: (κ + η) ∘ₖ μ = κ ∘ₖ μ + η ∘ₖ μ.

LaTeX

$$$ (\kappa + \eta) \circ_K \mu = \kappa \circ_K \mu + \eta \circ_K \mu $$$

Lean4

theorem comp_add_left (μ : Kernel α β) (κ η : Kernel β γ) : (κ + η) ∘ₖ μ = κ ∘ₖ μ + η ∘ₖ μ :=
  by
  ext a s hs
  simp_rw [comp_apply' _ _ _ hs, add_apply, Measure.add_apply, comp_apply' _ _ _ hs,
    lintegral_add_left (Kernel.measurable_coe κ hs)]

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