numeric_of_isEmpty_rightMoves — Mathlib

English

If the right moves of x are empty and every left move x.moveLeft i is numeric, then x is numeric.

Русский

Если правые ходы x пусты и каждый левый ход x.moveLeft i числовой, то x числовое.

LaTeX

$$$IsEmpty(x.RightMoves) \Rightarrow (\forall i : x.LeftMoves, Numeric(x.moveLeft(i)) ) \Rightarrow Numeric(x)$$$

Lean4

theorem numeric_of_isEmpty_rightMoves (x : PGame) [IsEmpty x.RightMoves] (H : ∀ i, Numeric (x.moveLeft i)) :
    Numeric x :=
  Numeric.mk (fun _ => isEmptyElim) H isEmptyElim

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