moveLeft_lf

Mathlib.SetTheory.PGame.Order

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

English

For every i, the i-th move of the left options satisfies moveLeft i ⧏ x.

Русский

Для каждого i выполняется moveLeft i ⧏ x.

LaTeX

$$$$ \\forall i, \\; (x.moveLeft i) \\;⧏\\; x. $$$$

Lean4

theorem moveLeft_lf {x : PGame} : ∀ i, x.moveLeft i ⧏ x :=
  le_rfl.moveLeft_lf

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

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

Разделы

Аффилиация

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