zero_le — Mathlib

English

For every pre-game x, 0 ≤ x if and only if for every right move j there exists a left move i such that 0 ≤ (x.moveRight j).moveLeft i.

Русский

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

LaTeX

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

Lean4

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

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