map_prod_eq — Mathlib

English

For kernels κ: α→β and η: α→γ, and a measurable f: β→δ, κ.map f ×K η equals (κ ×K η).map (Prod.map f id).

Русский

Для κ: α→β и η: α→γ и измеримого f: β→δ верно: (κ.map f) ×K η = (κ ×K η).map (Prod.map f id).

LaTeX

$$$\\displaystyle (\\kappa.map f) \\times_K \\eta = (\\kappa \\times_K \\eta).map (Prod.map f id)$$$

Lean4

theorem map_prod_eq (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] {f : β → δ}
    (hf : Measurable f) : (κ.map f) ×ₖ η = (κ ×ₖ η).map (Prod.map f id) := by
  rw [← map_prod_map _ _ hf measurable_id, map_id]

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