swap_apply_right

Mathlib.Logic.Equiv.Basic

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

English

Let a and b be elements of a type α. The transposition swapping a and b sends b to a.

Русский

Пусть a и b — элементы множества α. Транспозиция swap(a,b) отображает b в a.

LaTeX

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

Lean4

@[simp]
theorem swap_apply_right (a b : α) : swap a b b = a := by by_cases h : b = a <;> simp [swap_apply_def, h]

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

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

Разделы

Аффилиация

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