zero_lf — Mathlib

English

There exists a left move i such that for every right move j of the resulting game (x.moveLeft i).moveRight j, we have 0 ⧏ that game.

Русский

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

LaTeX

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

Lean4

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

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