moveLeft_impartial

Mathlib.SetTheory.Game.Impartial

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

English

If G is impartial, then for every left move i, G.moveLeft i is impartial.

Русский

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

LaTeX

$$$\forall i,\operatorname{Impartial}(G.moveLeft(i))$$$

Lean4

instance moveLeft_impartial {G : PGame} [h : G.Impartial] (i : G.LeftMoves) : (G.moveLeft i).Impartial :=
  (impartial_def.1 h).2.1 i

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

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

Разделы

Аффилиация

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