sumSumSumComm_symm — Mathlib

English

For all spaces X, Y, W, Z, the inverse of the triple sum commutativity homeomorphism coincides with the triple sum commutativity homeomorphism after swapping the middle two blocks. In symbols, the symmetry of sumSumSumComm gives (sumSumSumComm X Y W Z)^{−1} = sumSumSumComm X W Y Z.

Русский

Для всех пространств X, Y, W, Z обратная гомеоморфия тройной суммирующей перестановки совпадает с гомеоморфией тройной суммирующей перестановки при обмене средних двух блоков.

LaTeX

$$$ (\\mathrm{sumSumSumComm } X Y W Z)^{-1} = \\mathrm{sumSumSumComm } X W Y Z $$$

Lean4

@[simp]
theorem sumSumSumComm_symm : (sumSumSumComm X Y W Z).symm = (sumSumSumComm X W Y Z) :=
  rfl

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