map_comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem map_comp (κ : Kernel α β) (η : Kernel β γ) (f : γ → δ) : (η ∘ₖ κ).map f = (η.map f) ∘ₖ κ :=
  by
  by_cases hf : Measurable f
  · ext a s hs
    rw [map_apply' _ hf _ hs, comp_apply', comp_apply' _ _ _ hs]
    · simp_rw [map_apply' _ hf _ hs]
    · exact hf hs
  · simp [map_of_not_measurable _ hf]

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