lf_moveRight_of_le

Mathlib.SetTheory.PGame.Order

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

English

If x ≤ y, then for every j in y.RightMoves, x.LF (y.moveRight j).

Русский

Если x ≤ y, то для каждого j в y.RightMoves выполняется x.LF (y.moveRight j).

LaTeX

$$$ x \\le y \\;\\Rightarrow\\; \\forall j : y.RightMoves,\\ x \\text{LF} (y.moveRight j). $$$

Lean4

theorem lf_moveRight_of_le {x y : PGame} (h : x ≤ y) (j) : x ⧏ y.moveRight j :=
  (le_iff_forall_lf.1 h).2 j

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

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

Разделы

Аффилиация

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