mk — Mathlib · SciLib

English

A game x is numeric if all its Left moves are numeric and all its Right moves are numeric, and every Left move is strictly less than every Right move.

Русский

Игра x является числовой, если все её левые ходы числовые, все её правые ходы числовые, и каждый левый ход строго меньше каждого правого.

LaTeX

$$(∀ i : x.LeftMoves, Numeric (x.moveLeft i)) ∧ (∀ j : x.RightMoves, Numeric (x.moveRight j)) ∧ (∀ i : x.LeftMoves, ∀ j : x.RightMoves, x.moveLeft i < x.moveRight j) ⇒ Numeric x$$

Lean4

theorem mk {x : PGame} (h₁ : ∀ i j, x.moveLeft i < x.moveRight j) (h₂ : ∀ i, Numeric (x.moveLeft i))
    (h₃ : ∀ j, Numeric (x.moveRight j)) : Numeric x :=
  numeric_def.2 ⟨h₁, h₂, h₃⟩

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