map_prodMkRight — Mathlib

English

For any γ, κ, f, the mapping commutes with prodMkRight: map (prodMkRight γ κ) f = prodMkRight γ (map κ f).

Русский

Для любого γ, κ, f отображение коммутирует с prodMkRight: map (prodMkRight γ κ) f = prodMkRight γ (map κ f).

LaTeX

$$$\operatorname{map}(\operatorname{prodMkRight} \gamma \kappa) f = \operatorname{prodMkRight} \gamma (\operatorname{map} \kappa f)$$$

Lean4

theorem map_prodMkRight (κ : Kernel α β) (γ : Type*) {mγ : MeasurableSpace γ} (f : β → δ) :
    map (prodMkRight γ κ) f = prodMkRight γ (map κ f) :=
  by
  by_cases hf : Measurable f
  · simp only [map, hf, ↓reduceDIte]
    rfl
  · simp [map_of_not_measurable _ hf]

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