Conway names, the simplicity hierarchy and the surreal number tree

PHILIP EHRLICH

A tree ⟨A,<ₛ⟩ is a partially ordered class such that for each x ∈ A, the class {y ∈ A : y <ₛ x} of predecessors of x, written ‘pr_A(x)’, is a set well ordered by <ₛ.

We prove that the usual ordering of ℕ is a tree in this sense.

def «term_<ₛ_» : Lean.TrailingParserDescr

Equations

• «term_<ₛ_» = Lean.ParserDescr.trailingNode `«term_<ₛ_» 10 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <ₛ ") (Lean.ParserDescr.cat `term 0))

def «term_≤ₛ_» : Lean.TrailingParserDescr

Equations

• «term_≤ₛ_» = Lean.ParserDescr.trailingNode `«term_≤ₛ_» 10 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ₛ ") (Lean.ParserDescr.cat `term 0))