swapCore_swapCore — Mathlib

English

Applying swapCore twice with the same pair returns the original element: swapCore(a,b, swapCore(a,b,r)) = r.

Русский

Дважду подряд применение swapCore с теми же аргументами возвращает исходный элемент: swapCore(a,b, swapCore(a,b,r)) = r.

LaTeX

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

Lean4

theorem swapCore_swapCore (r a b : α) : swapCore a b (swapCore a b r) = r := by unfold swapCore; split_ifs <;> grind

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