swap_leftInverse — Mathlib

English

The swap operation on a sum type has a left-inverse with itself, i.e., applying swap twice returns the original element.

Русский

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

LaTeX

$$$$ \\mathrm{Sum.swap} \\circ \\mathrm{Sum.swap} = \\mathrm{id}. $$$$

Lean4

@[simp]
theorem swap_leftInverse : Function.LeftInverse (@swap α β) swap :=
  swap_swap

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