lf_zero_le — Mathlib

English

Let x be a pre-game. The relation x ⧏ 0 holds exactly when there exists a right move j with x.moveRight j ≤ 0.

Русский

Пусть x — предигра. Условие x ⧏ 0 выполняется тогда и только тогда, когда существует правый ход j такой, что x.moveRight j ≤ 0.

LaTeX

$$$x ⧏ 0 \Longleftrightarrow \exists j\, x.moveRight j \le 0$$$

Lean4

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

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