le_zero — Mathlib

English

For any pre-game x, x ≤ 0 holds exactly when every Left move i can be followed by some Right move j to stay below 0; i.e., (x.moveLeft i).moveRight j ≤ 0 for some j.

Русский

Для любого пред-игры x выполняется x ≤ 0 тогда и только тогда, когда для каждого хода слева i существует ход справа j, такой что (x.moveLeft i).moveRight j ≤ 0.

LaTeX

$$$x \le 0 \\iff \\forall i, \\exists j, (x.moveLeft i).moveRight j \\le 0$$$

Lean4

/-- The definition of `x ≤ 0` on pre-games, in terms of `≤ 0` two moves later. -/
theorem le_zero {x : PGame} : x ≤ 0 ↔ ∀ i, ∃ j, (x.moveLeft i).moveRight j ≤ 0 :=
  by
  rw [le_def]
  simp

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