map_prod_swap — Mathlib

English

The kernel map of the product with a swap equals the swapped product: map (κ ×K η) Prod.swap = η ×K κ.

Русский

Карта произведения с перестановкой равна переставленному произведению: map (κ ×K η) Prod.swap = η ×K κ.

LaTeX

$$$\\displaystyle \\text{map} (\\kappa \\times_K \\eta) \\; Prod.swap = \\eta \\times_K \\kappa$$$

Lean4

theorem map_prod_swap (κ : Kernel α β) (η : Kernel α γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    map (κ ×ₖ η) Prod.swap = η ×ₖ κ := by
  rw [ext_fun_iff]
  intro x f hf
  rw [lintegral_map _ measurable_swap _ hf, lintegral_prod, lintegral_prod _ _ _ hf]
  swap; · fun_prop
  refine (lintegral_lintegral_swap ?_).symm
  fun_prop

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