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}

@[implicit_reducible, instance 100]

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.

@[implicit_reducible]

instance OrderType.instAdd : Add OrderType.{u}

Equations

• OrderType.instAdd = { add := fun (o₁ o₂ : OrderType.{?u.1}) => o₁ + o₂ }

@[simp]

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

@[implicit_reducible]

instance OrderType.instAddMonoid : AddMonoid OrderType.{u}

Equations

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

@[implicit_reducible, instance 100]

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.

@[implicit_reducible]

instance OrderType.instMul : Mul OrderType.{u}

Equations

• OrderType.instMul = { mul := fun (o₁ o₂ : OrderType.{?u.1}) => o₁ * o₂ }

@[simp]

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

@[implicit_reducible]

instance OrderType.instMonoid : Monoid OrderType.{u}

Equations

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

def OrderType.card (o : OrderType.{u_1}) : Cardinal.{u_1}

The cardinal of an OrderType is the cardinality of any type on which a relation with that order type is defined.

Equations

• o.card = o.liftOn (fun (α : Type ?u.1) (x : LinearOrder α) => Cardinal.mk α) OrderType.card._proof_1✝

@[simp]

theorem OrderType.card_type {α : Type u} [LinearOrder α] : (type α).card = Cardinal.mk α

theorem OrderType.card_mono {o₁ o₂ : OrderType.{u_1}} : o₁ ≤ o₂ → o₁.card ≤ o₂.card

theorem OrderType.card_monotone : Monotone card

@[simp]

theorem OrderType.card_zero : card 0 = 0

@[simp]

theorem OrderType.card_one : card 1 = 1

@[implicit_reducible]

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 ℚ

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.

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 "θ")