Main definitions

• OrderType.card o: the cardinality of an OrderType o.
• o₁ + o₂: the lexicographic sum of order types, which forms an AddMonoid.
• o₁ * o₂: the lexicographic product of order types, which forms a MonoidWithZero.

Notation

The following are notations in the OrderType namespace:

• η is a notation for the order type of ℚ with its natural order.
• θ is a notation for the order type of ℝ with its natural order.

References

• https://en.wikipedia.org/wiki/Order_type
• [Dauben, J. W., Georg Cantor: His Mathematics and Philosophy of the Infinite. Princeton, NJ: Princeton University Press, 1990.][dauben_1990]
• [Enderton, Herbert B., Elements of Set Theory. United Kingdom: Academic Press, 1977.][enderton_1977]

Tags

order type, order isomorphism, linear order

instance OrderType.instZeroLEOneClass : ZeroLEOneClass OrderType.{u_1}

@[implicit_reducible, instance 100]

instance OrderType.instHAdd : HAdd OrderType.{u} OrderType.{v} OrderType.{max u v}

@[implicit_reducible]

instance OrderType.instAdd : Add OrderType.{u}

@[simp]

theorem OrderType.type_lex_sum (α : Type u) (β : Type v) [LinearOrder α] [LinearOrder β] : type (Lex (α ⊕ β)) = type α + type β

@[implicit_reducible]

instance OrderType.instAddMonoid : AddMonoid OrderType.{u}

@[implicit_reducible, instance 100]

instance OrderType.instHMul : HMul OrderType.{u} OrderType.{v} OrderType.{max u v}

@[implicit_reducible]

instance OrderType.instMul : Mul OrderType.{u}

@[simp]

theorem OrderType.type_lex_prod (α : Type u) (β : Type v) [LinearOrder α] [LinearOrder β] : type (Lex (α × β)) = type β * type α

@[implicit_reducible]

instance OrderType.instMonoid : Monoid OrderType.{u}

@[implicit_reducible]

instance OrderType.instOfNat (n : ℕ) : OfNat OrderType.{0} n

instance OrderType.instLeftDistribClass : LeftDistribClass OrderType.{u_1}

def OrderType.eta : OrderType.{0}

The order type of the rational numbers.

Conventions for notations in identifiers:

• The recommended spelling of η in identifiers is eta.

noncomputable def OrderType.theta : OrderType.{0}

The order type of the real numbers.

Conventions for notations in identifiers:

• The recommended spelling of θ in identifiers is theta.

def OrderType.termη : Lean.ParserDescr

The order type of the rational numbers.

Conventions for notations in identifiers:

• The recommended spelling of η in identifiers is eta.

def OrderType.termθ : Lean.ParserDescr

The order type of the real numbers.

Conventions for notations in identifiers:

• The recommended spelling of θ in identifiers is theta.