mk_rightMovesEquiv

Mathlib.SetTheory.PGame.Basic

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.Relabelling.mk_rightMovesEquiv

English

The rightMovesEquiv of a relabelling mk equals R.

Русский

Правовая ходовая эквивалентность relabelling mk равна R.

LaTeX

$$$ \text{mk rightMovesEquiv} = R $$$

Lean4

@[simp]
theorem mk_rightMovesEquiv {x y L R hL hR} : (@Relabelling.mk x y L R hL hR).rightMovesEquiv = R :=
  rfl

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

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

Разделы

Аффилиация

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