Surreal — Mathlib

English

For x with numeric witness o and i in LeftMoves, Surreal.mk(x.moveLeft i) (Numeric.moveLeft o i) < Surreal.mk x o.

Русский

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

LaTeX

$$$Surreal.mk(x.moveLeft(i))(Numeric.moveLeft(o,i)) < Surreal.mk(x)(o)$$$

Lean4

/-- The type of surreal numbers. These are the numeric pre-games quotiented
by the equivalence relation `x ≈ y ↔ x ≤ y ∧ y ≤ x`. In the quotient,
the order becomes a total order. -/
def Surreal :=
  Quotient (inferInstanceAs <| Setoid (Subtype Numeric))

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