zero_lf_le — Mathlib

English

Let x be a pre-game. The relation 0 ⧏ x holds exactly when there exists a left move i for which 0 ≤ x.moveLeft i.

Русский

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

LaTeX

$$$0 ⧏ x \Longleftrightarrow \exists i\, 0 \le x.moveLeft i$$$

Lean4

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

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