Declare type aliases of Ordinal

This repository contains two type aliases of Ordinal, each preserving the order structure but with distinct arithmetic defined on it, namely NatOrdinal and Nimber. We define a ordinal_alias! macro which contains all the boilerplate required to set up these types. This also ensures that the API between both stays consistent.

For Mathlib

theorem Ordinal.eq_natCast_of_le_natCast {a : Ordinal.{u_1}} {b : ℕ} (h : a ≤ ↑b) : ∃ (c : ℕ), a = ↑c

theorem Ordinal.Iio_zero : Set.Iio 0 = ∅

@[simp]

theorem Ordinal.Iio_one : Set.Iio 1 = {0}

@[simp]

theorem Ordinal.Iio_two : Set.Iio 2 = {0, 1}

Auxiliary defs

Macros

def commandAlias!___ : Lean.ParserDescr

Declare a type alias of either Ordinal or Nat, preserving the order structure.

Equations

• One or more equations did not get rendered due to their size.

def commandOrdinal_alias!__ : Lean.ParserDescr

Declare a type alias of Ordinal, preserving the order structure.

Equations

• One or more equations did not get rendered due to their size.