mk_lt_mk_moveRight — Mathlib

English

For x with numeric witness o and j in RightMoves, Surreal.mk x o < Surreal.mk (x.moveRight j) (Numeric.moveRight o j).

Русский

Для x с числовым свидетельством o и j из RightMoves, Surreal.mk x o < Surreal.mk (x.moveRight j) (Numeric.moveRight o j).

LaTeX

$$$Surreal.mk x o < Surreal.mk (x.moveRight j) (Numeric.moveRight o j)$$$

Lean4

/-- Same as `lt_moveRight`, but for `Surreal` instead of `PGame` -/
theorem mk_lt_mk_moveRight {x : PGame} (o : Numeric x) (j) :
    Surreal.mk x o < Surreal.mk (x.moveRight j) (Numeric.moveRight o j) :=
  Numeric.lt_moveRight o j

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