mk_moveLeft_lt_mk — Mathlib

English

Moving the left option on both sides yields a strictly smaller surreal than the original.

Русский

Левый ход слева приводит к строго меньшему сюрреалу по сравнению с исходным.

LaTeX

$$$\\mathrm{mk}(x.moveLeft(i), \\mathrm{Numeric.moveLeft}(o,i)) < \\mathrm{mk}(x,o)$$$

Lean4

/-- Same as `moveLeft_lt`, but for `Surreal` instead of `PGame` -/
theorem mk_moveLeft_lt_mk {x : PGame} (o : Numeric x) (i) :
    Surreal.mk (x.moveLeft i) (Numeric.moveLeft o i) < Surreal.mk x o :=
  Numeric.moveLeft_lt o i

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