swapCore_self

Mathlib.Logic.Equiv.Basic

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

English

For any r ∈ α and a ∈ α, swapCore a a r = r; swapping a with itself is identity.

Русский

Для любых r ∈ α и a ∈ α, swapCore a a r = r; обмен a с самим собой — тождественность.

LaTeX

$$$\\text{swapCore}(a,a,r)=r$$$

Lean4

theorem swapCore_self (r a : α) : swapCore a a r = r :=
  by
  unfold swapCore
  split_ifs <;> simp [*]

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

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

Разделы

Аффилиация

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