lf_moveRight

Mathlib.SetTheory.PGame.Order

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

English

For every j in the right moves, x LF (x.moveRight j).

Русский

Для каждого j из правых ходов x LF (x.moveRight j).

LaTeX

$$$$ \\forall j, \\; x \\;\\mathbf{LF}\\; (x.moveRight j). $$$$

Lean4

theorem lf_moveRight {x : PGame} : ∀ j, x ⧏ x.moveRight j :=
  le_rfl.lf_moveRight

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

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

Разделы

Аффилиация

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