gameAdd_swap_swap_mk

Mathlib.Order.GameAdd

URI: https://scilib.ai/kg/mathlib#Prod.gameAdd_swap_swap_mk

← MathLib Explorer

English

A restatement of the swap lemma specialized to mk form.

Русский

Специализированное формулирование леммы о перестановке для формы mk.

LaTeX

$$$\\text{gameAdd\_swap\_swap\_mk}$$$

Lean4

theorem gameAdd_swap_swap_mk (a₁ a₂ : α) (b₁ b₂ : β) :
    GameAdd rα rβ (a₁, b₁) (a₂, b₂) ↔ GameAdd rβ rα (b₁, a₁) (b₂, a₂) :=
  gameAdd_swap_swap rβ rα (b₁, a₁) (b₂, a₂)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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