def Ordinal.withBotOrderIso {α : Type u} [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] : (fun (x1 x2 : WithBot α) => x1 < x2) ≃r Sum.Lex EmptyRelation fun (x1 x2 : α) => x1 < x2

Equations

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

@[simp]

theorem Ordinal.type_withBot {α : Type u} [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] : (Ordinal.type fun (x1 x2 : WithBot α) => x1 < x2) = 1 + Ordinal.type fun (x1 x2 : α) => x1 < x2

theorem Ordinal.noMaxOrder_of_isLimit {α : Type u} [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] (h : (Ordinal.type fun (x1 x2 : α) => x1 < x2).IsLimit) : NoMaxOrder α

theorem Ordinal.isLimit_of_noMaxOrder {α : Type u} [Nonempty α] [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] (h : NoMaxOrder α) : (Ordinal.type fun (x1 x2 : α) => x1 < x2).IsLimit

theorem Ordinal.isLimit_iff_noMaxOrder {α : Type u} [Nonempty α] [Preorder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] : (Ordinal.type fun (x1 x2 : α) => x1 < x2).IsLimit ↔ NoMaxOrder α

theorem Ordinal.type_Iio_lt {α : Type u} [LtWellOrder α] (x : α) : Ordinal.type (Subrel (fun (x1 x2 : α) => x1 < x2) (Set.Iio x)) < Ordinal.type fun (x1 x2 : α) => x1 < x2

def Ordinal.iicOrderIso {α : Type u} [LtWellOrder α] (x : α) : Subrel (fun (x1 x2 : α) => x1 < x2) (Set.Iic x) ≃r Sum.Lex (Subrel (fun (x1 x2 : α) => x1 < x2) (Set.Iio x)) EmptyRelation

Equations

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

theorem Ordinal.type_Iic_eq {α : Type u} [LtWellOrder α] (x : α) : Ordinal.type (Subrel (fun (x1 x2 : α) => x1 < x2) (Set.Iic x)) = Ordinal.type (Subrel (fun (x1 x2 : α) => x1 < x2) (Set.Iio x)) + 1

theorem Ordinal.type_Iic_lt {α : Type u} [LtWellOrder α] [NoMaxOrder α] (x : α) : Ordinal.type (Subrel (fun (x1 x2 : α) => x1 < x2) (Set.Iic x)) < Ordinal.type fun (x1 x2 : α) => x1 < x2

Lifting ordinals

theorem Ordinal.ULift.isTrichotomous {α : Type u} {r : α → α → Prop} [IsTrichotomous α r] : IsTrichotomous (ULift.{v, u} α) (InvImage r ULift.down)

theorem Ordinal.ULift.isTrans {α : Type u} {r : α → α → Prop} [IsTrans α r] : IsTrans (ULift.{v, u} α) (InvImage r ULift.down)

theorem Ordinal.ULift.isWellOrder {α : Type u} {r : α → α → Prop} [IsWellOrder α r] : IsWellOrder (ULift.{v, u} α) (InvImage r ULift.down)

theorem Ordinal.lift_typein_apply {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : r ≼i s) (a : α) : Ordinal.lift.{max u v, v} ((Ordinal.typein s).toRelEmbedding (f a)) = Ordinal.lift.{max u v, u} ((Ordinal.typein r).toRelEmbedding a)

The additive structure on the set of ordinals below a cardinal

theorem Ordinal.card_Iio (o : Ordinal.{u}) : Cardinal.mk ↑(Set.Iio o) = Cardinal.lift.{u + 1, u} o.card

instance Ordinal.instLtWellOrderElemIio {o : Ordinal.{u}} : LtWellOrder ↑(Set.Iio o)

Equations

• Ordinal.instLtWellOrderElemIio = LtWellOrder.mk

theorem Ordinal.type_Iio (o : Ordinal.{u}) : (Ordinal.type fun (x1 x2 : ↑(Set.Iio o)) => x1 < x2) = Ordinal.lift.{u + 1, u} o

@[simp]

theorem Ordinal.typein_Iio {o : Ordinal.{u}} (x : ↑(Set.Iio o)) : (Ordinal.typein fun (x1 x2 : ↑(Set.Iio o)) => x1 < x2).toRelEmbedding x = Ordinal.lift.{u + 1, u} ↑x

theorem Ordinal.add_lt_ord {c : Cardinal.{u}} (h : Cardinal.aleph0 ≤ c) {x y : Ordinal.{u}} (hx : x < c.ord) (hy : y < c.ord) : x + y < c.ord

def Ordinal.iioAdd {c : Cardinal.{u}} (h : Cardinal.aleph0 ≤ c) : Add ↑(Set.Iio c.ord)

Equations

• Ordinal.iioAdd h = { add := fun (x y : ↑(Set.Iio c.ord)) => ⟨↑x + ↑y, ⋯⟩ }

def Ordinal.iioSub (o : Ordinal.{u_1}) : Sub ↑(Set.Iio o)

Equations

• o.iioSub = { sub := fun (x y : ↑(Set.Iio o)) => ⟨↑x - ↑y, ⋯⟩ }

theorem Ordinal.ord_pos {c : Cardinal.{u}} (h : Cardinal.aleph0 ≤ c) : 0 < c.ord

def Ordinal.iioZero {c : Cardinal.{u}} (h : Cardinal.aleph0 ≤ c) : Zero ↑(Set.Iio c.ord)

Equations

• Ordinal.iioZero h = { zero := ⟨0, ⋯⟩ }

@[simp]

theorem Ordinal.iioAdd_def {c : Cardinal.{u}} (h : Cardinal.aleph0 ≤ c) (x y : ↑(Set.Iio c.ord)) : ↑(x + y) = ↑x + ↑y

def Ordinal.iioAddMonoid {c : Cardinal.{u}} (h : Cardinal.aleph0 ≤ c) : AddMonoid ↑(Set.Iio c.ord)

Equations

• Ordinal.iioAddMonoid h = AddMonoid.mk ⋯ ⋯ nsmulRec ⋯ ⋯

theorem Ordinal.nat_lt_ord {c : Cardinal.{u}} (h : Cardinal.aleph0 ≤ c) (n : ℕ) : ↑n < c.ord

def Ordinal.iioOfNat {c : Cardinal.{u}} (h : Cardinal.aleph0 ≤ c) (n : ℕ) : OfNat (↑(Set.Iio c.ord)) n

Equations

• Ordinal.iioOfNat h n = { ofNat := ⟨↑n, ⋯⟩ }

theorem Ordinal.iioOfNat_coe {c : Cardinal.{u}} (h : Cardinal.aleph0 ≤ c) (n : ℕ) : ↑(OfNat.ofNat n) = ↑n

theorem Ordinal.iio_noMaxOrder {c : Cardinal.{u}} (h : Cardinal.aleph0 ≤ c) : NoMaxOrder ↑(Set.Iio c.ord)