prodComm_prod — Mathlib

English

The product commutes with the swap under a suitable measurable equivalence: (κ ×η).map MeasurableEquiv.prodComm equals η ×K κ.

Русский

Производное сопряжение с перестановкой через эквивалент сохраняется: (κ ×η).map MeasurableEquiv.prodComm = η ×K κ.

LaTeX

$$$\\displaystyle (\\kappa.\\times_K \\eta).map (\\mathrm{MeasurableEquiv}.prodComm) = \\eta \\times_K \\kappa$$$

Lean4

theorem prodComm_prod {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel α γ} [IsSFiniteKernel η] :
    (κ ×ₖ η).map MeasurableEquiv.prodComm = η ×ₖ κ :=
  map_prod_swap κ η

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