lf_of_le_moveLeft

Mathlib.SetTheory.PGame.Order

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

English

If x ≤ y.moveLeft i for some i, then x ⧏ y.

Русский

Если x ≤ y.moveLeft i для некоторого i, то x ⧏ y.

LaTeX

$$$ x \\le y.moveLeft i \\Rightarrow x \\;⧏\\; y. $$$

Lean4

theorem lf_of_le_moveLeft {x y : PGame} {i} (h : x ≤ y.moveLeft i) : x ⧏ y :=
  lf_iff_exists_le.2 <| Or.inl ⟨i, h⟩

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

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

Разделы

Аффилиация

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