sumComm_symm — Mathlib

English

The swap equivalence is its own inverse, i.e., swapping the two components twice yields the original order. Equivalently, (sumComm α β)^{-1} = sumComm β α.

Русский

Обмен эквивалентностей является своей собственной обратной операцией: обмен местами дважды возвращает исходный порядок. Эквивалентно, (sumComm α β)^{-1} = sumComm β α.

LaTeX

$$$$(\mathrm{sumComm}\,\alpha\,\beta)^{-1} = \mathrm{sumComm}\,\beta\,\alpha.$$$

Lean4

@[simp]
theorem sumComm_symm (α β) : (sumComm α β).symm = sumComm β α :=
  rfl

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