swap_apply_self — Mathlib

English

A function is an involution: applying swap twice yields the identity. Specifically, (swap i j) (swap i j a) = a.

Русский

Функция является инволютивной: применение swap дважды даёт тождественную отображение, т.е. swap(i,j)(swap(i,j)(a)) = a.

LaTeX

$$$(\mathrm{swap}(i,j))( \mathrm{swap}(i,j)(a) ) = a$$$

Lean4

@[simp]
theorem swap_apply_self (i j a : α) : swap i j (swap i j a) = a := by
  rw [← Equiv.trans_apply, Equiv.swap_swap, Equiv.refl_apply]

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