swap_comm

Mathlib.Logic.Equiv.Basic

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

English

Swapping two elements is symmetric: swap(a,b) = swap(b,a).

Русский

Обмен двух элементов обратим и симметричен: swap(a,b) = swap(b,a).

LaTeX

$$$\\text{swap}(a,b) = \\text{swap}(b,a)$$$

Lean4

theorem swap_comm (a b : α) : swap a b = swap b a :=
  ext fun r => swapCore_comm r _ _

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

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

Разделы

Аффилиация

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