sumComm_symm — Mathlib

English

The inverse of the sum-commutation is itself with swapped factors: (OrderIso.sumComm α β).symm = OrderIso.sumComm β α.

Русский

Обратный к перестановке сумм — то же самое отображение, но с переставленными аргументами: (OrderIso.sumComm α β).symm = OrderIso.sumComm β α.

LaTeX

$$$ (OrderIso.sumComm\, \alpha\, \beta).\mathrm{symm} = OrderIso.sumComm\, \beta\, \alpha $$$

Lean4

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

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