zero_le_lf

Mathlib.SetTheory.PGame.Order

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

← MathLib Explorer

English

0 ≤ x iff 0 ⧏ x.moveRight j for all j.

Русский

0 ≤ x эквивалентно тому, что 0 ⧏ x.moveRight j для всех j.

LaTeX

$$$$ 0 \\le x \\iff \\forall j, 0 \\;⧏\\; x.moveRight j. $$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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