moveRight_impartial

Mathlib.SetTheory.Game.Impartial

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.Impartial.moveRight_impartial

English

If G is impartial, then for every right move j, G.moveRight j is impartial.

Русский

Если G непредвзята, то для каждого правого хода j игра G.moveRight j непредвзята.

LaTeX

$$$\forall j,\operatorname{Impartial}(G.moveRight(j))$$$

Lean4

instance moveRight_impartial {G : PGame} [h : G.Impartial] (j : G.RightMoves) : (G.moveRight j).Impartial :=
  (impartial_def.1 h).2.2 j

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

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

Разделы

Аффилиация

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