comp_map — Mathlib

English

For κ: Kernel α β, η: Kernel γ δ and f: β → γ with measurability, η ∘ₖ (κ.map f) = (η.comap f) ∘ₖ κ.

Русский

Для κ: α → β, η: γ → δ и измеримого f: β → γ, η ∘ₖ (κ.map f) = (η.comap f) ∘ₖ κ.

LaTeX

$$$ η \circ_K (κ.map f) = (η.comap f) \circ_K κ $$$

Lean4

theorem comp_map (κ : Kernel α β) (η : Kernel γ δ) {f : β → γ} (hf : Measurable f) :
    η ∘ₖ (κ.map f) = (η.comap f hf) ∘ₖ κ := by
  ext x s ms
  rw [comp_apply' _ _ _ ms, lintegral_map _ hf _ (η.measurable_coe ms), comp_apply' _ _ _ ms]
  simp_rw [comap_apply']

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