swap_apply_left

Mathlib.Logic.Equiv.Basic

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

English

Applying swap to its left argument yields the right argument: swap a b a = b.

Русский

Применяя swap к левой аргумент, получаем правый: swap a b a = b.

LaTeX

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

Lean4

@[simp]
theorem swap_apply_left (a b : α) : swap a b a = b :=
  if_pos rfl

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

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

Разделы

Аффилиация

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