prodAssoc_symm_prod — Mathlib

English

The symmetric form of associativity holds with prodAssoc.symm: (κ × (ξ × η)).map prodAssoc.symm = (κ × ξ) × η.

Русский

Симметричная форма ассоциативности сохраняется через prodAssoc.symm: (κ × (ξ × η)).map prodAssoc.symm = (κ × ξ) × η.

LaTeX

$$$\\displaystyle (\\kappa \\times_K (\\xi \\times_K \\eta)).map (\\mathrm{prodAssoc}.symm) = (\\kappa \\times_K \\xi) \\times_K \\eta$$$

Lean4

theorem prodAssoc_symm_prod (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] (ξ : Kernel α δ)
    [IsSFiniteKernel ξ] : (κ ×ₖ (ξ ×ₖ η)).map MeasurableEquiv.prodAssoc.symm = (κ ×ₖ ξ) ×ₖ η :=
  by
  rw [← prodAssoc_prod, ← Kernel.map_comp_right _ (by fun_prop) (by fun_prop)]
  simp

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