map_prodMkLeft — Mathlib

English

For any γ, κ, f, the operation of mapping after prodMkLeft equals prodMkLeft of the mapped kernel: map (prodMkLeft γ κ) f = prodMkLeft γ (map κ f).

Русский

Для любого γ, κ, f выполнено: map (prodMkLeft γ κ) f = prodMkLeft γ (map κ f).

LaTeX

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

Lean4

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

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