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.
• Enderton, Herbert B. Elements of Set Theory. United Kingdom: Academic Press, 1977.

Tags

order type, order isomorphism, linear order

instance OrderType.instZeroLEOneClass : ZeroLEOneClass OrderType.{u_1}

instance OrderType.instAdd : Add OrderType.{u}

Equations

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

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

Equations

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

@[simp]

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

instance OrderType.instAddMonoid : AddMonoid OrderType.{u}

Equations

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

instance OrderType.instMul : Mul OrderType.{u}

Equations

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

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

Equations

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

@[simp]

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

instance OrderType.instMonoid : Monoid OrderType.{u}

Equations

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

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

Equations

• OrderType.instOfNat n = { ofNat := OrderType.type (Fin 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.

Equations

• OrderType.eta = OrderType.type ℚ

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.

Equations

• OrderType.theta = OrderType.type ℝ

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.

Equations

• OrderType.termη = Lean.ParserDescr.node `OrderType.termη 1024 (Lean.ParserDescr.symbol "η")

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.

Equations

• OrderType.termθ = Lean.ParserDescr.node `OrderType.termθ 1024 (Lean.ParserDescr.symbol "θ")