lf_zero — Mathlib

English

There exists a right move j such that for all left moves i of (x.moveRight j), we have (x.moveRight j).moveLeft i ⧏ 0.

Русский

Существует правый ход j, при котором для всех левых ходов i у x.moveRight j выполняется (x.moveRight j).moveLeft i ⧏ 0.

LaTeX

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

Lean4

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

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