swap_swap — Mathlib

English

The transposition swap(a,b) is an involution; applying it twice yields the identity.

Русский

Перестановка swap(a,b) — это инволютивная; дважды её применение даёт тождественную перестановку.

LaTeX

$$$(\mathrm{swap}(a,b)) \circ (\mathrm{swap}(a,b)) = \mathrm{id}$$$

Lean4

@[simp]
theorem swap_swap (a b : α) : (swap a b).trans (swap a b) = Equiv.refl _ :=
  ext fun _ => swapCore_swapCore _ _ _

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