swap_rightInverse — Mathlib

English

The swap map is also its own right inverse: applying swap twice yields the original element.

Русский

Отображение обмена также является собственной правой обратной: применение swap дважды возвращает исходный элемент.

LaTeX

$$$\\\\forall x, \\\\operatorname{swap}(\\\\operatorname{swap}(x)) = x.$$$

Lean4

@[simp]
theorem swap_rightInverse : Function.RightInverse (@swap α β) swap :=
  swap_swap

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