swap_self

Mathlib.Logic.Equiv.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.swap_self

English

For any a, swap a a = identity permutation.

Русский

Для любого a, swap a a равна тождественной перестановке.

LaTeX

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

Lean4

@[simp]
theorem swap_self (a : α) : swap a a = Equiv.refl _ :=
  ext fun r => swapCore_self r a

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru