le_zero_lf

Mathlib.SetTheory.PGame.Order

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

← MathLib Explorer

English

x ≤ 0 iff for all moves, x.moveLeft i ⧏ 0.

Русский

x ≤ 0 эквивалентно тому, что для каждого левого хода x.moveLeft i ⧏ 0.

LaTeX

$$$$ x \\le 0 \\iff \\forall i, x.moveLeft i \\\\mathbf{⧏} 0. $$$$

Lean4

/-- The definition of `x ≤ 0` on pre-games, in terms of `⧏ 0`. -/
theorem le_zero_lf {x : PGame} : x ≤ 0 ↔ ∀ i, x.moveLeft i ⧏ 0 :=
  by
  rw [le_iff_forall_lf]
  simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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