swap_eq_update — Mathlib

English

The swap permutation can be written as a double update of the identity: swap i j equals update(update id j i) i j.

Русский

Перестановку swap можно записать как двойное обновление функции: swap i j = update(update id j i) i j.

LaTeX

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

Lean4

theorem swap_eq_update (i j : α) : (Equiv.swap i j : α → α) = update (update id j i) i j :=
  funext fun x => by rw [update_apply _ i j, update_apply _ j i, Equiv.swap_apply_def, id]

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