swapCore_comm

Mathlib.Logic.Equiv.Basic

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

English

Swapping a and b in swapCore does not depend on order: swapCore(a,b,r) = swapCore(b,a,r).

Русский

Обмен местами a и b в swapCore не зависит от порядка: swapCore(a,b,r) = swapCore(b,a,r).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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