Documentation

Mathlib.SetTheory.Ordinal.Family

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.

Equations

Instances For

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.

Equations

Instances For

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.

Equations

Instances For

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.

Equations

Instances For

@[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.

Equations

Instances For

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_1 : 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 #

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] :

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.

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.

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.

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.

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

theorem Ordinal.iSup_eq_zero_iff {ι : Type u_4} {f : ι → Ordinal.{u}} [Small.{u, u_4} ι] :

iSup f = 0 ↔ ∀ (i : ι), f i = 0

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 iSup_succ (since := "2025-10-08")]

theorem Ordinal.iSup_succ {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] [SuccOrder α] (x : α) :

⨆ (a : ↑(Set.Iio x)), Order.succ ↑a = x

Alias of iSup_succ.

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

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)

@[deprecated Order.IsNormal.map_iSup (since := "2025-12-25")]

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

f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

@[deprecated Order.IsNormal.map_iSup (since := "2025-12-25")]

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

f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

@[deprecated Order.IsNormal.map_sSup (since := "2025-12-25")]

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

f (sSup s) = sSup (f '' s)

@[deprecated Order.IsNormal.map_sSup (since := "2025-12-25")]

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

f (sSup s) = sSup (f '' s)

@[deprecated Order.IsNormal.apply_of_isSuccLimit (since := "2025-12-25")]

theorem Ordinal.IsNormal.apply_of_isSuccLimit {f : Ordinal.{u} → Ordinal.{v}} (H : Ordinal.IsNormal f) {o : Ordinal.{u}} (ho : Order.IsSuccLimit o) :

f o = ⨆ (a : ↑(Set.Iio o)), f ↑a

theorem Ordinal.sSup_ord (s : Set Cardinal.{u_4}) :

(sSup s).ord = sSup (Cardinal.ord '' s)

theorem Ordinal.iSup_ord {ι : Sort u_4} (f : ι → Cardinal.{u_5}) :

(⨆ (i : ι), f i).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.iSup_eq_iSup {ι ι' : 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.{u_4}) :

iSup (familyOfBFamily' r ho f) = iSup (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 iSup over the family provided by familyOfBFamily.

Equations

Instances For

@[simp]

theorem Ordinal.iSup_eq_bsup {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}) :

iSup (o.familyOfBFamily f) = o.bsup f

theorem Ordinal.iSup'_eq_bsup {o : Ordinal.{u_4}} {ι : Type u_4} (r : ι → ι → Prop) [IsWellOrder ι r] (ho : type r = o) (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}) :

iSup (familyOfBFamily' r ho f) = o.bsup f

theorem Ordinal.sSup_eq_bsup {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}) :

sSup (o.brange f) = o.bsup f

@[simp]

theorem Ordinal.bsup'_eq_iSup {ι : Type u_4} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u_4 u_5}) :

(type r).bsup (bfamilyOfFamily' r f) = iSup f

@[simp]

theorem Ordinal.bsup_eq_iSup {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

(type WellOrderingRel).bsup (bfamilyOfFamily f) = iSup 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)

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_4 u_5} → Ordinal.{max u_5 u_6}} (H : Order.IsNormal f) {o : Ordinal.{u_5}} (g : (a : Ordinal.{u_5}) → a < o → Ordinal.{max u_5 u_4}) :

o ≠ 0 → f (o.bsup g) = o.bsup fun (a : Ordinal.{u_5}) (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_1 : 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_Iio_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

@[deprecated Ordinal.iSup_eq_iSup (since := "2025-10-01")]

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.{u_4}) :

iSup (familyOfBFamily' r ho f) = iSup (familyOfBFamily' r' ho' f)

Alias of Ordinal.iSup_eq_iSup.

@[deprecated Ordinal.iSup'_eq_bsup (since := "2025-10-01")]

theorem Ordinal.sup_eq_bsup' {o : Ordinal.{u_4}} {ι : Type u_4} (r : ι → ι → Prop) [IsWellOrder ι r] (ho : type r = o) (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}) :

iSup (familyOfBFamily' r ho f) = o.bsup f

Alias of Ordinal.iSup'_eq_bsup.

@[deprecated Ordinal.iSup_eq_bsup (since := "2025-10-01")]

theorem Ordinal.sup_eq_bsup {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}) :

iSup (o.familyOfBFamily f) = o.bsup f

Alias of Ordinal.iSup_eq_bsup.

@[deprecated Ordinal.bsup'_eq_iSup (since := "2025-10-01")]

theorem Ordinal.bsup_eq_sup' {ι : Type u_4} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → Ordinal.{max u_4 u_5}) :

(type r).bsup (bfamilyOfFamily' r f) = iSup f

Alias of Ordinal.bsup'_eq_iSup.

@[deprecated Ordinal.bsup_eq_iSup (since := "2025-10-01")]

theorem Ordinal.bsup_eq_sup {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

(type WellOrderingRel).bsup (bfamilyOfFamily f) = iSup f

Alias of Ordinal.bsup_eq_iSup.

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

Ordinal.{max u v}

The least strict upper bound of a family of ordinals.

Equations

Instances For

@[simp]

theorem Ordinal.iSup_eq_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

iSup (Order.succ ∘ f) = lsub f

theorem Ordinal.lsub_le_iff {ι : Type u_4} {f : ι → Ordinal.{max u_5 u_4}} {a : Ordinal.{max u_4 u_5}} :

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_4} {f : ι → Ordinal.{max u_5 u_4}} {a : Ordinal.{max u_4 u_5}} :

a < lsub f ↔ ∃ (i : ι), a ≤ f i

theorem Ordinal.iSup_le_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

iSup f ≤ lsub f

theorem Ordinal.lsub_le_succ_iSup {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

lsub f ≤ Order.succ (iSup f)

theorem Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

iSup f = lsub f ∨ Order.succ (iSup f) = lsub f

theorem Ordinal.succ_iSup_le_lsub_iff {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

Order.succ (iSup f) ≤ lsub f ↔ ∃ (i : ι), f i = iSup f

theorem Ordinal.succ_iSup_eq_lsub_iff {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

Order.succ (iSup f) = lsub f ↔ ∃ (i : ι), f i = iSup f

theorem Ordinal.iSup_eq_lsub_iff {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

iSup f = lsub f ↔ ∀ a < lsub f, Order.succ a < lsub f

theorem Ordinal.iSup_eq_lsub_iff_lt_iSup {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

iSup f = lsub f ↔ ∀ (i : ι), f i < iSup 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_4} [h : Nonempty ι] (f : ι → Ordinal.{max u_5 u_4}) :

0 < lsub f

@[simp]

theorem Ordinal.lsub_eq_zero_iff {ι : Type u_4} (f : ι → Ordinal.{max v u_4}) :

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_4} (f : ι → Ordinal.{max u_5 u_4}) :

lsub f ∉ Set.range f

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.iSup_typein_limit {o : Ordinal.{u}} (ho : ∀ a < o, Order.succ a < o) :

iSup ⇑(typein fun (x1 x2 : o.ToType) => x1 < x2).toRelEmbedding = o

@[simp]

theorem Ordinal.iSup_typein_succ {o : Ordinal.{u_4}} :

iSup ⇑(typein fun (x1 x2 : (Order.succ o).ToType) => x1 < x2).toRelEmbedding = o

@[deprecated Ordinal.iSup_eq_lsub (since := "2025-10-01")]

theorem Ordinal.sup_eq_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

iSup (Order.succ ∘ f) = lsub f

Alias of Ordinal.iSup_eq_lsub.

@[deprecated Ordinal.iSup_le_lsub (since := "2025-10-01")]

theorem Ordinal.sup_le_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

iSup f ≤ lsub f

Alias of Ordinal.iSup_le_lsub.

@[deprecated Ordinal.lsub_le_succ_iSup (since := "2025-10-01")]

theorem Ordinal.lsub_le_sup_succ {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

lsub f ≤ Order.succ (iSup f)

Alias of Ordinal.lsub_le_succ_iSup.

@[deprecated Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub (since := "2025-10-01")]

theorem Ordinal.sup_eq_lsub_or_sup_succ_eq_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

iSup f = lsub f ∨ Order.succ (iSup f) = lsub f

Alias of Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub.

@[deprecated Ordinal.succ_iSup_le_lsub_iff (since := "2025-10-01")]

theorem Ordinal.sup_succ_le_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

Order.succ (iSup f) ≤ lsub f ↔ ∃ (i : ι), f i = iSup f

Alias of Ordinal.succ_iSup_le_lsub_iff.

@[deprecated Ordinal.succ_iSup_eq_lsub_iff (since := "2025-10-01")]

theorem Ordinal.sup_succ_eq_lsub {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

Order.succ (iSup f) = lsub f ↔ ∃ (i : ι), f i = iSup f

Alias of Ordinal.succ_iSup_eq_lsub_iff.

@[deprecated Ordinal.iSup_eq_lsub_iff (since := "2025-10-01")]

theorem Ordinal.sup_eq_lsub_iff_succ {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

iSup f = lsub f ↔ ∀ a < lsub f, Order.succ a < lsub f

Alias of Ordinal.iSup_eq_lsub_iff.

@[deprecated Ordinal.iSup_eq_lsub_iff_lt_iSup (since := "2025-10-01")]

theorem Ordinal.sup_eq_lsub_iff_lt_sup {ι : Type u_4} (f : ι → Ordinal.{max u_5 u_4}) :

iSup f = lsub f ↔ ∀ (i : ι), f i < iSup f

Alias of Ordinal.iSup_eq_lsub_iff_lt_iSup.

@[deprecated Ordinal.iSup_typein_limit (since := "2025-10-01")]

theorem Ordinal.sup_typein_limit {o : Ordinal.{u}} (ho : ∀ a < o, Order.succ a < o) :

iSup ⇑(typein fun (x1 x2 : o.ToType) => x1 < x2).toRelEmbedding = o

Alias of Ordinal.iSup_typein_limit.

@[deprecated Ordinal.iSup_typein_succ (since := "2025-10-01")]

theorem Ordinal.sup_typein_succ {o : Ordinal.{u_4}} :

iSup ⇑(typein fun (x1 x2 : (Order.succ o).ToType) => x1 < x2).toRelEmbedding = o

Alias of Ordinal.iSup_typein_succ.

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.

Equations

Instances For

@[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 u_4}) :

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_1 : 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 : Order.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 : Order.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}} :

Order.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}} :

Order.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

@[deprecated Order.IsNormal.ext (since := "2025-12-25")]

theorem Ordinal.IsNormal.eq_iff_zero_and_succ {f g : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (hg : Order.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_1} [Small.{u, u_1} α] (f : α → Ordinal.{u}) :

¬Function.Surjective f

theorem not_injective_of_ordinal {α : Type u_1} [Small.{u, u_1} α] (f : Ordinal.{u} → α) :

¬Function.Injective f

@[deprecated not_surjective_of_ordinal (since := "2025-08-21")]

theorem not_surjective_of_ordinal_of_small {α : Type u_1} [Small.{u, u_1} α] (f : α → Ordinal.{u}) :

¬Function.Surjective f

Alias of not_surjective_of_ordinal.

@[deprecated not_injective_of_ordinal (since := "2025-08-21")]

theorem not_injective_of_ordinal_of_small {α : Type u_1} [Small.{u, u_1} α] (f : Ordinal.{u} → α) :

¬Function.Injective f

Alias of not_injective_of_ordinal.

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.apply_omega0_of_isNormal {f : Ordinal.{u} → Ordinal.{v}} (hf : Order.IsNormal f) :

⨆ (n : ℕ), f ↑n = f omega0

@[deprecated Ordinal.apply_omega0_of_isNormal (since := "2025-12-25")]

theorem Ordinal.IsNormal.apply_omega0 {f : Ordinal.{u} → Ordinal.{v}} (hf : Order.IsNormal f) :

⨆ (n : ℕ), f ↑n = f omega0

Alias of Ordinal.apply_omega0_of_isNormal.

@[simp]

theorem Ordinal.iSup_add_natCast (o : Ordinal.{u_1}) :

⨆ (n : ℕ), o + ↑n = o + omega0

@[deprecated Ordinal.iSup_add_natCast (since := "2025-12-25")]

theorem Ordinal.iSup_add_nat (o : Ordinal.{u_1}) :

⨆ (n : ℕ), o + ↑n = o + omega0

Alias of Ordinal.iSup_add_natCast.

@[simp]

theorem Ordinal.iSup_mul_natCast (o : Ordinal.{u_1}) :

⨆ (n : ℕ), o * ↑n = o * omega0

@[deprecated Ordinal.iSup_mul_natCast (since := "2025-12-25")]

theorem Ordinal.iSup_mul_nat (o : Ordinal.{u_1}) :

⨆ (n : ℕ), o * ↑n = o * omega0

Alias of Ordinal.iSup_mul_natCast.