symm_swap

Mathlib.Logic.Equiv.Basic

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

English

The inverse of the swap is the swap itself.

Русский

Обратная перестановка swap — та же перестановка.

LaTeX

$$$(\mathrm{swap}(a,b))^{-1} = \mathrm{swap}(a,b)$$$

Lean4

@[simp]
theorem symm_swap (a b : α) : (swap a b).symm = swap a b :=
  rfl

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

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

Разделы

Аффилиация

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