Arithmetic on families of ordinals

Main definitions and results

• sup, lsub: the supremum / least strict upper bound of an indexed family of ordinals in Type u, as an ordinal in Type u.
• bsup, blsub: the supremum / least strict upper bound of a set of ordinals indexed by ordinals less than a given ordinal o.

Various other basic arithmetic results are given in Principal.lean instead.

Families of ordinals

There are two kinds of indexed families that naturally arise when dealing with ordinals: those indexed by some type in the appropriate universe, and those indexed by ordinals less than another. The following API allows one to convert from one kind of family to the other.

In many cases, this makes it easy to prove claims about one kind of family via the corresponding claim on the other.

def Ordinal.bfamilyOfFamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (a : Ordinal.{u}) : a < type r → α

Converts a family indexed by a Type u to one indexed by an Ordinal.{u} using a specified well-ordering.

def Ordinal.bfamilyOfFamily {α : Type u_1} {ι : Type u} : (ι → α) → (a : Ordinal.{u}) → a < type WellOrderingRel → α

Converts a family indexed by a Type u to one indexed by an Ordinal.{u} using a well-ordering given by the axiom of choice.

def Ordinal.familyOfBFamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : type r = o) (f : (a : Ordinal.{u}) → a < o → α) : ι → α

Converts a family indexed by an Ordinal.{u} to one indexed by a Type u using a specified well-ordering.

def Ordinal.familyOfBFamily {α : Type u_1} (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < o → α) : o.toType → α

Converts a family indexed by an Ordinal.{u} to one indexed by a Type u using a well-ordering given by the axiom of choice.

@[simp]

theorem Ordinal.bfamilyOfFamily'_typein {α : Type u_1} {ι : Type u_4} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (i : ι) : bfamilyOfFamily' r f ((typein r).toRelEmbedding i) ⋯ = f i

@[simp]

theorem Ordinal.bfamilyOfFamily_typein {α : Type u_1} {ι : Type u_4} (f : ι → α) (i : ι) : bfamilyOfFamily f ((typein WellOrderingRel).toRelEmbedding i) ⋯ = f i

theorem Ordinal.familyOfBFamily'_enum {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : type r = o) (f : (a : Ordinal.{u}) → a < o → α) (i : Ordinal.{u}) (hi : i < o) : familyOfBFamily' r ho f ((enum r) ⟨i, ⋯⟩) = f i hi

theorem Ordinal.familyOfBFamily_enum {α : Type u_1} (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < o → α) (i : Ordinal.{u_4}) (hi : i < o) : o.familyOfBFamily f ((enum fun (x1 x2 : o.toType) => x1 < x2) ⟨i, ⋯⟩) = f i hi

def Ordinal.brange {α : Type u_1} (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < o → α) : Set α

The range of a family indexed by ordinals.

theorem Ordinal.mem_brange {α : Type u_1} {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → α} {a : α} : a ∈ o.brange f ↔ ∃ (i : Ordinal.{u_4}) (hi : i < o), f i hi = a

theorem Ordinal.mem_brange_self {α : Type u_1} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → α) (i : Ordinal.{u_4}) (hi : i < o) : f i hi ∈ o.brange f

@[simp]

theorem Ordinal.range_familyOfBFamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : type r = o) (f : (a : Ordinal.{u}) → a < o → α) : Set.range (familyOfBFamily' r ho f) = o.brange f

@[simp]

theorem Ordinal.range_familyOfBFamily {α : Type u_1} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → α) : Set.range (o.familyOfBFamily f) = o.brange f

@[simp]

theorem Ordinal.brange_bfamilyOfFamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) : (type r).brange (bfamilyOfFamily' r f) = Set.range f

@[simp]

theorem Ordinal.brange_bfamilyOfFamily {α : Type u_1} {ι : Type u} (f : ι → α) : (type WellOrderingRel).brange (bfamilyOfFamily f) = Set.range f

@[simp]

theorem Ordinal.brange_const {α : Type u_1} {o : Ordinal.{u_4}} (ho : o ≠ 0) {c : α} : (o.brange fun (x : Ordinal.{u_4}) (x : x < o) => c) = {c}

theorem Ordinal.comp_bfamilyOfFamily' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (g : α → β) : (fun (i : Ordinal.{u}) (hi : i < type r) => g (bfamilyOfFamily' r f i hi)) = bfamilyOfFamily' r (g ∘ f)

theorem Ordinal.comp_bfamilyOfFamily {α : Type u_1} {β : Type u_2} {ι : Type u} (f : ι → α) (g : α → β) : (fun (i : Ordinal.{u}) (hi : i < type WellOrderingRel) => g (bfamilyOfFamily f i hi)) = bfamilyOfFamily (g ∘ f)

theorem Ordinal.comp_familyOfBFamily' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : type r = o) (f : (a : Ordinal.{u}) → a < o → α) (g : α → β) : g ∘ familyOfBFamily' r ho f = familyOfBFamily' r ho fun (i : Ordinal.{u}) (hi : i < o) => g (f i hi)

theorem Ordinal.comp_familyOfBFamily {α : Type u_1} {β : Type u_2} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → α) (g : α → β) : g ∘ o.familyOfBFamily f = o.familyOfBFamily fun (i : Ordinal.{u_4}) (hi : i < o) => g (f i hi)

Supremum of a family of ordinals

@[deprecated iSup (since := "2024-08-27")]

def Ordinal.sup {ι : Type u} (f : ι → Ordinal.{max u v}) : Ordinal.{max u v}

The supremum of a family of ordinals

theorem Ordinal.bddAbove_range {ι : Type u} (f : ι → Ordinal.{max u v}) : BddAbove (Set.range f)

The range of an indexed ordinal function, whose outputs live in a higher universe than the inputs, is always bounded above. See Ordinal.lsub for an explicit bound.

theorem Ordinal.bddAbove_of_small (s : Set Ordinal.{u}) [h : Small.{u, u + 1} ↑s] : BddAbove s

theorem Ordinal.bddAbove_iff_small {s : Set Ordinal.{u}} : BddAbove s ↔ Small.{u, u + 1} ↑s

theorem Ordinal.bddAbove_image {s : Set Ordinal.{u}} (hf : BddAbove s) (f : Ordinal.{u} → Ordinal.{max u v}) : BddAbove (f '' s)

theorem Ordinal.bddAbove_range_comp {ι : Type u} {f : ι → Ordinal.{v}} (hf : BddAbove (Set.range f)) (g : Ordinal.{v} → Ordinal.{max v w}) : BddAbove (Set.range (g ∘ f))

theorem Ordinal.le_iSup {ι : Type u_4} (f : ι → Ordinal.{u}) [Small.{u, u_4} ι] (i : ι) : f i ≤ iSup f

le_ciSup whenever the input type is small in the output universe. This lemma sometimes fails to infer f in simple cases and needs it to be given explicitly.

@[deprecated Ordinal.le_iSup (since := "2024-08-27")]

theorem Ordinal.le_sup {ι : Type u} (f : ι → Ordinal.{max u v}) (i : ι) : f i ≤ sup f

theorem Ordinal.iSup_le_iff {ι : Type u_4} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_4} ι] : iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a

ciSup_le_iff' whenever the input type is small in the output universe.

@[deprecated Ordinal.iSup_le_iff (since := "2024-08-27")]

theorem Ordinal.sup_le_iff {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal.{max u v}} : sup f ≤ a ↔ ∀ (i : ι), f i ≤ a

theorem Ordinal.iSup_le {ι : Sort u_4} {f : ι → Ordinal.{u_5}} {a : Ordinal.{u_5}} : (∀ (i : ι), f i ≤ a) → iSup f ≤ a

An alias of ciSup_le' for discoverability.

@[deprecated Ordinal.iSup_le (since := "2024-08-27")]

theorem Ordinal.sup_le {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal.{max u v}} : (∀ (i : ι), f i ≤ a) → sup f ≤ a

theorem Ordinal.lt_iSup_iff {ι : Type u_4} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_4} ι] : a < iSup f ↔ ∃ (i : ι), a < f i

lt_ciSup_iff' whenever the input type is small in the output universe.

@[deprecated "No deprecation message was provided." (since := "2024-08-27")]

theorem Ordinal.ne_iSup_iff_lt_iSup {ι : Type u} {f : ι → Ordinal.{max u v}} : (∀ (i : ι), f i ≠ iSup f) ↔ ∀ (i : ι), f i < iSup f

@[deprecated Ordinal.ne_iSup_iff_lt_iSup (since := "2024-08-27")]

theorem Ordinal.ne_sup_iff_lt_sup {ι : Type u} {f : ι → Ordinal.{max u v}} : (∀ (i : ι), f i ≠ sup f) ↔ ∀ (i : ι), f i < sup f

theorem Ordinal.succ_lt_iSup_of_ne_iSup {ι : Type u_4} {f : ι → Ordinal.{u}} [Small.{u, u_4} ι] (hf : ∀ (i : ι), f i ≠ iSup f) {a : Ordinal.{u}} (hao : a < iSup f) : Order.succ a < iSup f

@[deprecated Ordinal.succ_lt_iSup_of_ne_iSup (since := "2024-08-27")]

theorem Ordinal.sup_not_succ_of_ne_sup {ι : Type u} {f : ι → Ordinal.{max u v}} (hf : ∀ (i : ι), f i ≠ sup f) {a : Ordinal.{max u v}} (hao : a < sup f) : Order.succ a < sup f

theorem Ordinal.iSup_eq_zero_iff {ι : Type u_4} {f : ι → Ordinal.{u}} [Small.{u, u_4} ι] : iSup f = 0 ↔ ∀ (i : ι), f i = 0

@[deprecated ciSup_const (since := "2024-08-27")]

theorem Ordinal.sup_const {ι : Type u_4} [_hι : Nonempty ι] (o : Ordinal.{max u_5 u_4}) : (sup fun (x : ι) => o) = o

@[deprecated ciSup_unique (since := "2024-08-27")]

theorem Ordinal.sup_unique {ι : Type u_4} [Unique ι] (f : ι → Ordinal.{max u_5 u_4}) : sup f = f default

@[deprecated csSup_le_csSup' (since := "2024-08-27")]

theorem Ordinal.sup_le_of_range_subset {ι : Type u} {ι' : Type v} {f : ι → Ordinal.{max (max u v) w}} {g : ι' → Ordinal.{max (max u v) w}} (h : Set.range f ⊆ Set.range g) : sup f ≤ sup g

theorem Ordinal.iSup_eq_of_range_eq {ι : Sort u_4} {ι' : Sort u_5} {f : ι → Ordinal.{u_6}} {g : ι' → Ordinal.{u_6}} (h : Set.range f = Set.range g) : iSup f = iSup g

@[deprecated Ordinal.iSup_eq_of_range_eq (since := "2024-08-27")]

theorem Ordinal.sup_eq_of_range_eq {ι : Type u} {ι' : Type v} {f : ι → Ordinal.{max u v w}} {g : ι' → Ordinal.{max u v w}} (h : Set.range f = Set.range g) : sup f = sup g

theorem Ordinal.iSup_succ (o : Ordinal.{u_4}) : ⨆ (a : ↑(Set.Iio o)), Order.succ ↑a = o

theorem Ordinal.iSup_sum {α : Type u_4} {β : Type u_5} (f : α ⊕ β → Ordinal.{u}) [Small.{u, u_4} α] [Small.{u, u_5} β] : iSup f = max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))

@[deprecated Ordinal.iSup_sum (since := "2024-08-27")]

theorem Ordinal.sup_sum {α : Type u} {β : Type v} (f : α ⊕ β → Ordinal.{max (max u v) w}) : sup f = max (sup fun (a : α) => f (Sum.inl a)) (sup fun (b : β) => f (Sum.inr b))

theorem Ordinal.unbounded_range_of_le_iSup {α β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β → α) (h : type r ≤ ⨆ (i : β), (typein r).toRelEmbedding (f i)) : Set.Unbounded r (Set.range f)

theorem Ordinal.IsNormal.map_iSup_of_bddAbove {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {ι : Type u_4} (g : ι → Ordinal.{u}) (hg : BddAbove (Set.range g)) [Nonempty ι] : f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

theorem Ordinal.IsNormal.map_iSup {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {ι : Type w} (g : ι → Ordinal.{u}) [Small.{u, w} ι] [Nonempty ι] : f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

theorem Ordinal.IsNormal.map_sSup_of_bddAbove {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {s : Set Ordinal.{u}} (hs : BddAbove s) (hn : s.Nonempty) : f (sSup s) = sSup (f '' s)

theorem Ordinal.IsNormal.map_sSup {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {s : Set Ordinal.{u}} (hn : s.Nonempty) [Small.{u, u + 1} ↑s] : f (sSup s) = sSup (f '' s)

@[deprecated Ordinal.IsNormal.map_iSup (since := "2024-08-27")]

theorem Ordinal.IsNormal.sup {f : Ordinal.{max u v} → Ordinal.{max u w}} (H : IsNormal f) {ι : Type u} (g : ι → Ordinal.{max u v}) [Nonempty ι] : f (Ordinal.sup g) = Ordinal.sup (f ∘ g)

theorem Ordinal.IsNormal.apply_of_isSuccLimit {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {o : Ordinal.{u}} (ho : Order.IsSuccLimit o) : f o = ⨆ (a : ↑(Set.Iio o)), f ↑a

@[deprecated Ordinal.IsNormal.apply_of_isSuccLimit (since := "2025-07-08")]

theorem Ordinal.IsNormal.apply_of_isLimit {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {o : Ordinal.{u}} (ho : Order.IsSuccLimit o) : f o = ⨆ (a : ↑(Set.Iio o)), f ↑a

Alias of Ordinal.IsNormal.apply_of_isSuccLimit.

theorem Ordinal.sSup_ord {s : Set Cardinal.{u}} (hs : BddAbove s) : (sSup s).ord = sSup (Cardinal.ord '' s)

theorem Ordinal.iSup_ord {ι : Sort u_4} {f : ι → Cardinal.{u_5}} (hf : BddAbove (Set.range f)) : (iSup f).ord = ⨆ (i : ι), (f i).ord

theorem Ordinal.lift_card_sInf_compl_le (s : Set Ordinal.{u}) : Cardinal.lift.{u + 1, u} (sInf sᶜ).card ≤ Cardinal.mk ↑s

theorem Ordinal.card_sInf_range_compl_le_lift {ι : Type u} (f : ι → Ordinal.{max u v}) : (sInf (Set.range f)ᶜ).card ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)

theorem Ordinal.card_sInf_range_compl_le {ι : Type u} (f : ι → Ordinal.{u}) : (sInf (Set.range f)ᶜ).card ≤ Cardinal.mk ι

theorem Ordinal.sInf_compl_lt_lift_ord_succ {ι : Type u} (f : ι → Ordinal.{max u v}) : sInf (Set.range f)ᶜ < lift.{v, u} (Order.succ (Cardinal.mk ι)).ord

theorem Ordinal.sInf_compl_lt_ord_succ {ι : Type u} (f : ι → Ordinal.{u}) : sInf (Set.range f)ᶜ < (Order.succ (Cardinal.mk ι)).ord

theorem Ordinal.sup_eq_sup {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : type r = o) (ho' : type r' = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : sup (familyOfBFamily' r ho f) = sup (familyOfBFamily' r' ho' f)

def Ordinal.bsup (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : Ordinal.{max u v}

The supremum of a family of ordinals indexed by the set of ordinals less than some o : Ordinal.{u}. This is a special case of sup over the family provided by familyOfBFamily.

@[simp]

theorem Ordinal.sup_eq_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : sup (o.familyOfBFamily f) = o.bsup f

@[simp]

theorem Ordinal.sup_eq_bsup' {o : Ordinal.{u}} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (ho : type r = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : sup (familyOfBFamily' r ho f) = o.bsup f

theorem Ordinal.sSup_eq_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : sSup (o.brange f) = o.bsup f

@[simp]

theorem Ordinal.bsup_eq_sup' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u v}) : (type r).bsup (bfamilyOfFamily' r f) = sup f

theorem Ordinal.bsup_eq_bsup {ι : Type u} (r r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r'] (f : ι → Ordinal.{max u v}) : (type r).bsup (bfamilyOfFamily' r f) = (type r').bsup (bfamilyOfFamily' r' f)

@[simp]

theorem Ordinal.bsup_eq_sup {ι : Type u} (f : ι → Ordinal.{max u v}) : (type WellOrderingRel).bsup (bfamilyOfFamily f) = sup f

theorem Ordinal.bsup_congr {o₁ o₂ : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}) (ho : o₁ = o₂) : o₁.bsup f = o₂.bsup fun (a : Ordinal.{u}) (h : a < o₂) => f a ⋯

theorem Ordinal.bsup_le_iff {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {a : Ordinal.{max u v}} : o.bsup f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h ≤ a

theorem Ordinal.bsup_le {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}} {a : Ordinal.{max u v}} : (∀ (i : Ordinal.{u}) (h : i < o), f i h ≤ a) → o.bsup f ≤ a

theorem Ordinal.le_bsup {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}) (i : Ordinal.{u_4}) (h : i < o) : f i h ≤ o.bsup f

theorem Ordinal.lt_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) {a : Ordinal.{max u v}} : a < o.bsup f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), a < f i hi

theorem Ordinal.IsNormal.bsup {f : Ordinal.{max u v} → Ordinal.{max u w}} (H : IsNormal f) {o : Ordinal.{u}} (g : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : o ≠ 0 → f (o.bsup g) = o.bsup fun (a : Ordinal.{u}) (h : a < o) => f (g a h)

theorem Ordinal.lt_bsup_of_ne_bsup {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} : (∀ (i : Ordinal.{u}) (h : i < o), f i h ≠ o.bsup f) ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f

theorem Ordinal.bsup_not_succ_of_ne_bsup {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} (hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ o.bsup f) (a : Ordinal.{max u v}) : a < o.bsup f → Order.succ a < o.bsup f

@[simp]

theorem Ordinal.bsup_eq_zero_iff {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}} : o.bsup f = 0 ↔ ∀ (i : Ordinal.{u_4}) (hi : i < o), f i hi = 0

theorem Ordinal.lt_bsup_of_limit {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}} (hf : ∀ {a a' : Ordinal.{u_4}} (ha : a < o) (ha' : a' < o), a < a' → f a ha < f a' ha') (ho : ∀ a < o, Order.succ a < o) (i : Ordinal.{u_4}) (h : i < o) : f i h < o.bsup f

theorem Ordinal.bsup_succ_of_mono {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < Order.succ o → Ordinal.{max u_4 u_5}} (hf : ∀ {i j : Ordinal.{u_4}} (hi : i < Order.succ o) (hj : j < Order.succ o), i ≤ j → f i hi ≤ f j hj) : (Order.succ o).bsup f = f o ⋯

@[simp]

theorem Ordinal.bsup_zero (f : (a : Ordinal.{u_4}) → a < 0 → Ordinal.{max u_4 u_5}) : bsup 0 f = 0

theorem Ordinal.bsup_const {o : Ordinal.{u}} (ho : o ≠ 0) (a : Ordinal.{max u v}) : (o.bsup fun (x : Ordinal.{u}) (x : x < o) => a) = a

@[simp]

theorem Ordinal.bsup_one (f : (a : Ordinal.{u_4}) → a < 1 → Ordinal.{max u_4 u_5}) : bsup 1 f = f 0 ⋯

theorem Ordinal.bsup_le_of_brange_subset {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}} {g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}} (h : o.brange f ⊆ o'.brange g) : o.bsup f ≤ o'.bsup g

theorem Ordinal.bsup_eq_of_brange_eq {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}} {g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}} (h : o.brange f = o'.brange g) : o.bsup f = o'.bsup g

theorem Ordinal.iSup_eq_bsup {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}} : ⨆ (a : ↑(Set.Iio o)), f ↑a ⋯ = o.bsup f

def Ordinal.lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) : Ordinal.{max u_5 u_4}

The least strict upper bound of a family of ordinals.

@[simp]

theorem Ordinal.sup_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : sup (Order.succ ∘ f) = lsub f

theorem Ordinal.lsub_le_iff {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal.{max v u}} : lsub f ≤ a ↔ ∀ (i : ι), f i < a

theorem Ordinal.lsub_le {ι : Type u_4} {f : ι → Ordinal.{max u_5 u_4}} {a : Ordinal.{max u_5 u_4}} : (∀ (i : ι), f i < a) → lsub f ≤ a

theorem Ordinal.lt_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) (i : ι) : f i < lsub f

theorem Ordinal.lt_lsub_iff {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal.{max v u}} : a < lsub f ↔ ∃ (i : ι), a ≤ f i

theorem Ordinal.sup_le_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : sup f ≤ lsub f

theorem Ordinal.lsub_le_sup_succ {ι : Type u} (f : ι → Ordinal.{max u v}) : lsub f ≤ Order.succ (sup f)

theorem Ordinal.sup_eq_lsub_or_sup_succ_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : sup f = lsub f ∨ Order.succ (sup f) = lsub f

theorem Ordinal.sup_succ_le_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : Order.succ (sup f) ≤ lsub f ↔ ∃ (i : ι), f i = sup f

theorem Ordinal.sup_succ_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : Order.succ (sup f) = lsub f ↔ ∃ (i : ι), f i = sup f

theorem Ordinal.sup_eq_lsub_iff_succ {ι : Type u} (f : ι → Ordinal.{max u v}) : sup f = lsub f ↔ ∀ a < lsub f, Order.succ a < lsub f

theorem Ordinal.sup_eq_lsub_iff_lt_sup {ι : Type u} (f : ι → Ordinal.{max u v}) : sup f = lsub f ↔ ∀ (i : ι), f i < sup f

@[simp]

theorem Ordinal.lsub_empty {ι : Type u_4} [h : IsEmpty ι] (f : ι → Ordinal.{max u_5 u_4}) : lsub f = 0

theorem Ordinal.lsub_pos {ι : Type u} [h : Nonempty ι] (f : ι → Ordinal.{max u v}) : 0 < lsub f

@[simp]

theorem Ordinal.lsub_eq_zero_iff {ι : Type u} (f : ι → Ordinal.{max u v}) : lsub f = 0 ↔ IsEmpty ι

@[simp]

theorem Ordinal.lsub_const {ι : Type u_4} [Nonempty ι] (o : Ordinal.{max u_5 u_4}) : (lsub fun (x : ι) => o) = Order.succ o

@[simp]

theorem Ordinal.lsub_unique {ι : Type u_4} [Unique ι] (f : ι → Ordinal.{max u_5 u_4}) : lsub f = Order.succ (f default)

theorem Ordinal.lsub_le_of_range_subset {ι : Type u} {ι' : Type v} {f : ι → Ordinal.{max (max u v) w}} {g : ι' → Ordinal.{max (max u v) w}} (h : Set.range f ⊆ Set.range g) : lsub f ≤ lsub g

theorem Ordinal.lsub_eq_of_range_eq {ι : Type u} {ι' : Type v} {f : ι → Ordinal.{max (max u v) w}} {g : ι' → Ordinal.{max (max u v) w}} (h : Set.range f = Set.range g) : lsub f = lsub g

@[simp]

theorem Ordinal.lsub_sum {α : Type u} {β : Type v} (f : α ⊕ β → Ordinal.{max (max u v) w}) : lsub f = max (lsub fun (a : α) => f (Sum.inl a)) (lsub fun (b : β) => f (Sum.inr b))

theorem Ordinal.lsub_notMem_range {ι : Type u} (f : ι → Ordinal.{max u v}) : lsub f ∉ Set.range f

@[deprecated Ordinal.lsub_notMem_range (since := "2025-05-23")]

theorem Ordinal.lsub_not_mem_range {ι : Type u} (f : ι → Ordinal.{max u v}) : lsub f ∉ Set.range f

Alias of Ordinal.lsub_notMem_range.

theorem Ordinal.nonempty_compl_range {ι : Type u} (f : ι → Ordinal.{max u v}) : (Set.range f)ᶜ.Nonempty

@[simp]

theorem Ordinal.lsub_typein (o : Ordinal.{u}) : lsub ⇑(typein fun (x1 x2 : o.toType) => x1 < x2).toRelEmbedding = o

theorem Ordinal.sup_typein_limit {o : Ordinal.{u}} (ho : ∀ a < o, Order.succ a < o) : sup ⇑(typein fun (x1 x2 : o.toType) => x1 < x2).toRelEmbedding = o

@[simp]

theorem Ordinal.sup_typein_succ {o : Ordinal.{u}} : sup ⇑(typein fun (x1 x2 : (Order.succ o).toType) => x1 < x2).toRelEmbedding = o

def Ordinal.blsub (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : Ordinal.{max u v}

The least strict upper bound of a family of ordinals indexed by the set of ordinals less than some o : Ordinal.{u}.

This is to lsub as bsup is to sup.

@[simp]

theorem Ordinal.bsup_eq_blsub (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : (o.bsup fun (a : Ordinal.{u}) (ha : a < o) => Order.succ (f a ha)) = o.blsub f

theorem Ordinal.lsub_eq_blsub' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : type r = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : lsub (familyOfBFamily' r ho f) = o.blsub f

theorem Ordinal.lsub_eq_lsub {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : type r = o) (ho' : type r' = o) (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : lsub (familyOfBFamily' r ho f) = lsub (familyOfBFamily' r' ho' f)

@[simp]

theorem Ordinal.lsub_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : lsub (o.familyOfBFamily f) = o.blsub f

@[simp]

theorem Ordinal.blsub_eq_lsub' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u v}) : (type r).blsub (bfamilyOfFamily' r f) = lsub f

theorem Ordinal.blsub_eq_blsub {ι : Type u} (r r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r'] (f : ι → Ordinal.{max u v}) : (type r).blsub (bfamilyOfFamily' r f) = (type r').blsub (bfamilyOfFamily' r' f)

@[simp]

theorem Ordinal.blsub_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : (type WellOrderingRel).blsub (bfamilyOfFamily f) = lsub f

theorem Ordinal.blsub_congr {o₁ o₂ : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}) (ho : o₁ = o₂) : o₁.blsub f = o₂.blsub fun (a : Ordinal.{u}) (h : a < o₂) => f a ⋯

theorem Ordinal.blsub_le_iff {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {a : Ordinal.{max u v}} : o.blsub f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < a

theorem Ordinal.blsub_le {o : Ordinal.{u_4}} {f : (b : Ordinal.{u_4}) → b < o → Ordinal.{max u_4 u_5}} {a : Ordinal.{max u_4 u_5}} : (∀ (i : Ordinal.{u_4}) (h : i < o), f i h < a) → o.blsub f ≤ a

theorem Ordinal.lt_blsub {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}) (i : Ordinal.{u_4}) (h : i < o) : f i h < o.blsub f

theorem Ordinal.lt_blsub_iff {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}} {a : Ordinal.{max u v}} : a < o.blsub f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), a ≤ f i hi

theorem Ordinal.bsup_le_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : o.bsup f ≤ o.blsub f

theorem Ordinal.blsub_le_bsup_succ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : o.blsub f ≤ Order.succ (o.bsup f)

theorem Ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : o.bsup f = o.blsub f ∨ Order.succ (o.bsup f) = o.blsub f

theorem Ordinal.bsup_succ_le_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : Order.succ (o.bsup f) ≤ o.blsub f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o.bsup f

theorem Ordinal.bsup_succ_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : Order.succ (o.bsup f) = o.blsub f ↔ ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o.bsup f

theorem Ordinal.bsup_eq_blsub_iff_succ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : o.bsup f = o.blsub f ↔ ∀ a < o.blsub f, Order.succ a < o.blsub f

theorem Ordinal.bsup_eq_blsub_iff_lt_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}) : o.bsup f = o.blsub f ↔ ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < o.bsup f

theorem Ordinal.bsup_eq_blsub_of_lt_succ_limit {o : Ordinal.{u}} (ho : Order.IsSuccLimit o) {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} (hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (Order.succ a) ⋯) : o.bsup f = o.blsub f

theorem Ordinal.blsub_succ_of_mono {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < Order.succ o → Ordinal.{max u v}} (hf : ∀ {i j : Ordinal.{u}} (hi : i < Order.succ o) (hj : j < Order.succ o), i ≤ j → f i hi ≤ f j hj) : (Order.succ o).blsub f = Order.succ (f o ⋯)

@[simp]

theorem Ordinal.blsub_eq_zero_iff {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}} : o.blsub f = 0 ↔ o = 0

@[simp]

theorem Ordinal.blsub_zero (f : (a : Ordinal.{u_4}) → a < 0 → Ordinal.{max u_4 u_5}) : blsub 0 f = 0

theorem Ordinal.blsub_pos {o : Ordinal.{u_4}} (ho : 0 < o) (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}) : 0 < o.blsub f

theorem Ordinal.blsub_type {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}) : (type r).blsub f = lsub fun (a : α) => f ((typein r).toRelEmbedding a) ⋯

theorem Ordinal.blsub_const {o : Ordinal.{u}} (ho : o ≠ 0) (a : Ordinal.{max u v}) : (o.blsub fun (x : Ordinal.{u}) (x : x < o) => a) = Order.succ a

@[simp]

theorem Ordinal.blsub_one (f : (a : Ordinal.{u_4}) → a < 1 → Ordinal.{max u_4 u_5}) : blsub 1 f = Order.succ (f 0 ⋯)

@[simp]

theorem Ordinal.blsub_id (o : Ordinal.{u}) : (o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => x) = o

theorem Ordinal.bsup_id_limit {o : Ordinal.{u}} : (∀ a < o, Order.succ a < o) → (o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => x) = o

@[simp]

theorem Ordinal.bsup_id_succ (o : Ordinal.{u}) : ((Order.succ o).bsup fun (x : Ordinal.{u}) (x_1 : x < Order.succ o) => x) = o

theorem Ordinal.blsub_le_of_brange_subset {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}} {g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}} (h : o.brange f ⊆ o'.brange g) : o.blsub f ≤ o'.blsub g

theorem Ordinal.blsub_eq_of_brange_eq {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}} {g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}} (h : {o_1 : Ordinal.{max (max u v) w} | ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o_1} = {o : Ordinal.{max (max u v) w} | ∃ (i : Ordinal.{v}) (hi : i < o'), g i hi = o}) : o.blsub f = o'.blsub g

theorem Ordinal.bsup_comp {o o' : Ordinal.{max u v}} {f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}} (hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj) {g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}} (hg : o'.blsub g = o) : (o'.bsup fun (a : Ordinal.{max u v}) (ha : a < o') => f (g a ha) ⋯) = o.bsup f

theorem Ordinal.blsub_comp {o o' : Ordinal.{max u v}} {f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}} (hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj) {g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}} (hg : o'.blsub g = o) : (o'.blsub fun (a : Ordinal.{max u v}) (ha : a < o') => f (g a ha) ⋯) = o.blsub f

theorem Ordinal.IsNormal.bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}} (H : IsNormal f) {o : Ordinal.{u}} (h : Order.IsSuccLimit o) : (o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o

theorem Ordinal.IsNormal.blsub_eq {f : Ordinal.{u} → Ordinal.{max u v}} (H : IsNormal f) {o : Ordinal.{u}} (h : Order.IsSuccLimit o) : (o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o

theorem Ordinal.isNormal_iff_lt_succ_and_bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}} : IsNormal f ↔ (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧ ∀ (o : Ordinal.{u}), Order.IsSuccLimit o → (o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o

theorem Ordinal.isNormal_iff_lt_succ_and_blsub_eq {f : Ordinal.{u} → Ordinal.{max u v}} : IsNormal f ↔ (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧ ∀ (o : Ordinal.{u}), Order.IsSuccLimit o → (o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o

theorem Ordinal.IsNormal.eq_iff_zero_and_succ {f g : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) (hg : IsNormal g) : f = g ↔ f 0 = g 0 ∧ ∀ (a : Ordinal.{u}), f a = g a → f (Order.succ a) = g (Order.succ a)

Results about injectivity and surjectivity

theorem not_surjective_of_ordinal {α : Type u} (f : α → Ordinal.{u}) : ¬Function.Surjective f

theorem not_injective_of_ordinal {α : Type u} (f : Ordinal.{u} → α) : ¬Function.Injective f

theorem not_surjective_of_ordinal_of_small {α : Type v} [Small.{u, v} α] (f : α → Ordinal.{u}) : ¬Function.Surjective f

theorem not_injective_of_ordinal_of_small {α : Type v} [Small.{u, v} α] (f : Ordinal.{u} → α) : ¬Function.Injective f

theorem not_small_ordinal : ¬Small.{u, max (u + 1) (v + 1)} Ordinal.{max u v}

The type of ordinals in universe u is not Small.{u}. This is the type-theoretic analog of the Burali-Forti paradox.

instance Ordinal.uncountable : Uncountable Ordinal.{u}

theorem Ordinal.not_bddAbove_compl_of_small (s : Set Ordinal.{u}) [hs : Small.{u, u + 1} ↑s] : ¬BddAbove sᶜ

Casting naturals into ordinals, compatibility with operations

@[simp]

theorem Ordinal.iSup_natCast : iSup Nat.cast = omega0

theorem Ordinal.IsNormal.apply_omega0 {f : Ordinal.{u} → Ordinal.{v}} (hf : IsNormal f) : ⨆ (n : ℕ), f ↑n = f omega0

@[simp]

theorem Ordinal.iSup_add_nat (o : Ordinal.{u_1}) : ⨆ (n : ℕ), o + ↑n = o + omega0

@[simp]

theorem Ordinal.iSup_mul_nat (o : Ordinal.{u_1}) : ⨆ (n : ℕ), o * ↑n = o * omega0