English
A swap-level commutation of comaps and prod-maps holds: comap (prodMkRight α η ×K prodMkLeft γ κ) Prod.swap = map (prodMkRight γ κ ×K prodMkLeft α η) Prod.swap.
Русский
Сдвиговый факт о комапах и отображениях: comap (prodMkRight α η ×K prodMkLeft γ κ) Prod.swap = map (prodMkRight γ κ ×K prodMkLeft α η) Prod.swap.
LaTeX
$$$\\displaystyle comap (prodMkRight\\ α\\ η \\times_K \\; prodMkLeft\\ γ\\ κ) Prod.swap = map (prodMkRight\\ γ\\ κ \\times_K \\; prodMkLeft\\ α\\ η) Prod.swap$$$
Lean4
theorem comap_prod_swap (κ : Kernel α β) (η : Kernel γ δ) [IsSFiniteKernel κ] [IsSFiniteKernel η] :
comap (prodMkRight α η ×ₖ prodMkLeft γ κ) Prod.swap measurable_swap =
map (prodMkRight γ κ ×ₖ prodMkLeft α η) Prod.swap :=
by
rw [ext_fun_iff]
intro x f hf
rw [lintegral_comap, lintegral_map _ measurable_swap _ hf, lintegral_prod _ _ _ hf, lintegral_prod]
swap; · fun_prop
simp only [prodMkRight_apply, Prod.fst_swap, Prod.swap_prod_mk, lintegral_prodMkLeft, Prod.snd_swap]
refine (lintegral_lintegral_swap ?_).symm
fun_prop
