Arithmetic on families of ordinals #

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

Ordinal.familyOfBFamily' r ho f i = f ((Ordinal.typein r).toRelEmbedding i) ⋯

Instances For

source

@[deprecated Ordinal.typein (since := "2026-04-06")]

def Ordinal.familyOfBFamily {α : Type u_1} (o : Ordinal.{u_3}) (f : (a : Ordinal.{u_3}) → 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

o.familyOfBFamily f = Ordinal.familyOfBFamily' (fun (x1 x2 : o.ToType) => x1 < x2) ⋯ f

Instances For

source

@[deprecated "bfamilyOfFamily is deprecated" (since := "2026-04-06")]

theorem Ordinal.bfamilyOfFamily'_typein {α : Type u_1} {ι : Type u_3} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (i : ι) :

bfamilyOfFamily' r f ((typein r).toRelEmbedding i) ⋯ = f i

source

@[deprecated "bfamilyOfFamily is deprecated" (since := "2026-04-06")]

theorem Ordinal.bfamilyOfFamily_typein {α : Type u_1} {ι : Type u_3} (f : ι → α) (i : ι) :

bfamilyOfFamily f ((typein WellOrderingRel).toRelEmbedding i) ⋯ = f i

source

@[deprecated "familyOfBFamily is deprecated" (since := "2026-04-06")]

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

source

@[deprecated "familyOfBFamily is deprecated" (since := "2026-04-06")]

theorem Ordinal.familyOfBFamily_enum {α : Type u_1} (o : Ordinal.{u_3}) (f : (a : Ordinal.{u_3}) → a < o → α) (i : Ordinal.{u_3}) (hi : i < o) :

o.familyOfBFamily f ((enum fun (x1 x2 : o.ToType) => x1 < x2) ⟨i, ⋯⟩) = f i hi

source

@[deprecated Set.range (since := "2026-04-06")]

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

Set α

The range of a family indexed by ordinals.

Equations

o.brange f = {a : α | ∃ (i : Ordinal.{?u.7}) (hi : i < o), f i hi = a}

Instances For

source

@[deprecated Set.mem_range (since := "2026-04-06")]

theorem Ordinal.mem_brange {α : Type u_1} {o : Ordinal.{u_3}} {f : (a : Ordinal.{u_3}) → a < o → α} {a : α} :

a ∈ o.brange f ↔ ∃ (i : Ordinal.{u_3}) (hi : i < o), f i hi = a

source

@[deprecated Set.mem_range_self (since := "2026-04-06")]

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

f i hi ∈ o.brange f

source

@[deprecated "familyOfBFamily is deprecated" (since := "2026-04-06")]

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

source

@[deprecated "familyOfBFamily is deprecated" (since := "2026-04-06")]

theorem Ordinal.range_familyOfBFamily {α : Type u_1} {o : Ordinal.{u_3}} (f : (a : Ordinal.{u_3}) → a < o → α) :

Set.range (o.familyOfBFamily f) = o.brange f

source

@[deprecated "bfamilyOfFamily is deprecated" (since := "2026-04-06")]

theorem Ordinal.brange_bfamilyOfFamily' {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) :

(type r).brange (bfamilyOfFamily' r f) = Set.range f

source

@[deprecated "bfamilyOfFamily is deprecated" (since := "2026-04-06")]

theorem Ordinal.brange_bfamilyOfFamily {α : Type u_1} {ι : Type u} (f : ι → α) :

(type WellOrderingRel).brange (bfamilyOfFamily f) = Set.range f

source

@[deprecated "brange is deprecated" (since := "2026-04-06")]

theorem Ordinal.brange_const {α : Type u_1} {o : Ordinal.{u_3}} (ho : o ≠ 0) {c : α} :

(o.brange fun (x : Ordinal.{u_3}) (x_1 : x < o) => c) = {c}

source

@[deprecated "bfamilyOfFamily is deprecated" (since := "2026-04-06")]

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)

source

@[deprecated "bfamilyOfFamily is deprecated" (since := "2026-04-06")]

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)

source

@[deprecated "familyOfBFamily is deprecated" (since := "2026-04-06")]

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)

source

@[deprecated "familyOfBFamily is deprecated" (since := "2026-04-06")]

theorem Ordinal.comp_familyOfBFamily {α : Type u_1} {β : Type u_2} {o : Ordinal.{u_3}} (f : (a : Ordinal.{u_3}) → a < o → α) (g : α → β) :

g ∘ o.familyOfBFamily f = o.familyOfBFamily fun (i : Ordinal.{u_3}) (hi : i < o) => g (f i hi)

Supremum of a family of ordinals #

source

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

BddAbove s

source

@[deprecated Ordinal.bddAbove_of_small (since := "2026-04-04")]

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

BddAbove (Set.range f)

source

theorem Ordinal.bddAbove_iff_small {s : Set Ordinal.{u}} :

BddAbove s ↔ Small.{u, u + 1} ↑s

source

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

BddAbove (f '' s)

source

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

source

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

f i ≤ ⨆ (i : ι), f i

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.

source

@[simp]

theorem Ordinal.iSup_le_iff {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι] :

⨆ (i : ι), f i ≤ a ↔ ∀ (i : ι), f i ≤ a

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

source

theorem Ordinal.iSup_le {ι : Sort u_3} {f : ι → Ordinal.{u_4}} {a : Ordinal.{u_4}} :

(∀ (i : ι), f i ≤ a) → ⨆ (i : ι), f i ≤ a

An alias of ciSup_le' for discoverability.

source

@[simp]

theorem Ordinal.lt_iSup_iff {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι] :

a < ⨆ (i : ι), f i ↔ ∃ (i : ι), a < f i

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

source

theorem Ordinal.lt_iSup_add_one {ι : Type u_3} (f : ι → Ordinal.{u}) [Small.{u, u_3} ι] (i : ι) :

f i < ⨆ (i : ι), f i + 1

source

theorem Ordinal.iSup_add_one_le_iff {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι] :

⨆ (i : ι), f i + 1 ≤ a ↔ ∀ (i : ι), f i < a

source

theorem Ordinal.iSup_add_one_le {ι : Sort u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} (h : ∀ (i : ι), f i < a) :

⨆ (i : ι), f i + 1 ≤ a

source

theorem Ordinal.lt_iSup_add_one_iff {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι] :

a < ⨆ (i : ι), f i + 1 ↔ ∃ (i : ι), a ≤ f i

source

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

Order.succ a < iSup f

source

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

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

source

@[deprecated congrArg (since := "2026-03-27")]

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

iSup f = iSup g

source

theorem Ordinal.iSup_sum {α : Type u_3} {β : Type u_4} (f : α ⊕ β → Ordinal.{u}) [Small.{u, u_3} α] [Small.{u, u_4} β] :

iSup f = max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))

source

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)

source

@[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_3} (g : ι → Ordinal.{u}) (hg : BddAbove (Set.range g)) [Nonempty ι] :

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

source

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

source

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

source

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

source

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

source

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

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

source

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

(⨆ (i : ι), f i).ord = ⨆ (i : ι), (f i).ord

source

theorem Ordinal.lift_card_sInf_compl_le (s : Set Ordinal.{u}) :

Cardinal.lift.{u + 1, u} (sInf sᶜ).card ≤ Cardinal.mk ↑s

source

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

source

theorem Ordinal.card_sInf_range_compl_le {ι : Type u} (f : ι → Ordinal.{u}) :

(sInf (Set.range f)ᶜ).card ≤ Cardinal.mk ι

source

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

source

theorem Ordinal.sInf_compl_lt_ord_succ {ι : Type u} (f : ι → Ordinal.{u}) :

sInf (Set.range f)ᶜ < (Order.succ (Cardinal.mk ι)).ord

source

theorem Ordinal.bddAbove_add_one_image_iff {s : Set Ordinal.{u_3}} :

BddAbove ((fun (x : Ordinal.{u_3}) => x + 1) '' s) ↔ BddAbove s

source

theorem Ordinal.bddAbove_range_add_one_iff {β : Type u_2} {f : β → Ordinal.{u}} :

BddAbove (Set.range fun (i : β) => f i + 1) ↔ BddAbove (Set.range f)

source

theorem Ordinal.sSup_le_sSup_add_one (s : Set Ordinal.{u_3}) :

sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) => x + 1) '' s)

source

theorem Ordinal.iSup_le_iSup_add_one {β : Type u_2} (f : β → Ordinal.{u_3}) :

⨆ (i : β), f i ≤ ⨆ (i : β), f i + 1

source

theorem Ordinal.iSup_add_one {β : Type u_3} [LinearOrder β] [NoMaxOrder β] {f : β → Ordinal.{u}} (hf : StrictMono f) :

⨆ (i : β), f i + 1 = ⨆ (i : β), f i

source

theorem Ordinal.iSup_Iio_add_one {a : Ordinal.{u}} {f : ↑(Set.Iio a) → Ordinal.{u}} (hf : StrictMono f) (ha : Order.IsSuccPrelimit a) :

⨆ (i : ↑(Set.Iio a)), f i + 1 = ⨆ (i : ↑(Set.Iio a)), f i

source

@[deprecated "familyOfBFamily is deprecated" (since := "2026-04-06")]

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_3}) :

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

source

@[deprecated "write `⨆ i : Iio a, f i` instead." (since := "2026-04-05")]

noncomputable 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

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

Instances For

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

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

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

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

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

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

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

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

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

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

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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)

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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 ⋯

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

f i h ≤ o.bsup f

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

source

@[deprecated Ordinal.IsNormal.map_iSup (since := "2026-04-05")]

theorem Ordinal.IsNormal.bsup {f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}} (H : Order.IsNormal f) {o : Ordinal.{u_4}} (g : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_3}) :

o ≠ 0 → f (o.bsup g) = o.bsup fun (a : Ordinal.{u_4}) (h : a < o) => f (g a h)

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

theorem Ordinal.bsup_eq_zero_iff {o : Ordinal.{u_3}} {f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}} :

o.bsup f = 0 ↔ ∀ (i : Ordinal.{u_3}) (hi : i < o), f i hi = 0

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

f i h < o.bsup f

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

theorem Ordinal.bsup_succ_of_mono {o : Ordinal.{u_3}} {f : (a : Ordinal.{u_3}) → a < Order.succ o → Ordinal.{max u_3 u_4}} (hf : ∀ {i j : Ordinal.{u_3}} (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 ⋯

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

bsup 0 f = 0

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

theorem Ordinal.bsup_one (f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}) :

bsup 1 f = f 0 ⋯

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

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

source

@[deprecated "bsup is deprecated" (since := "2026-04-05")]

theorem Ordinal.iSup_Iio_eq_bsup {o : Ordinal.{u_3}} {f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}} :

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

source

@[deprecated "write `⨆ i, f i + 1` instead." (since := "2026-03-27")]

noncomputable 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

Ordinal.lsub f = iSup (Order.succ ∘ f)

Instances For

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

iSup (Order.succ ∘ f) = lsub f

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

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

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

theorem Ordinal.lsub_le {ι : Type u_3} {f : ι → Ordinal.{max u_4 u_3}} {a : Ordinal.{max u_4 u_3}} :

(∀ (i : ι), f i < a) → lsub f ≤ a

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

f i < lsub f

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

theorem Ordinal.lt_lsub_iff {ι : Type u_3} {f : ι → Ordinal.{max u_4 u_3}} {a : Ordinal.{max u_3 u_4}} :

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

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

iSup f ≤ lsub f

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

lsub f ≤ Order.succ (iSup f)

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

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

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

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

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

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

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

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

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

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

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

theorem Ordinal.lsub_empty {ι : Type u_3} [h : IsEmpty ι] (f : ι → Ordinal.{max u_4 u_3}) :

lsub f = 0

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

theorem Ordinal.lsub_pos {ι : Type u_3} [h : Nonempty ι] (f : ι → Ordinal.{max u_4 u_3}) :

0 < lsub f

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

lsub f = 0 ↔ IsEmpty ι

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

theorem Ordinal.lsub_const {ι : Type u_3} [Nonempty ι] (o : Ordinal.{max u_4 u_3}) :

(lsub fun (x : ι) => o) = Order.succ o

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

theorem Ordinal.lsub_unique {ι : Type u_3} [Unique ι] (f : ι → Ordinal.{max u_4 u_3}) :

lsub f = Order.succ (f default)

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

theorem Ordinal.lsub_notMem_range {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}) :

lsub f ∉ Set.range f

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

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

(Set.range f)ᶜ.Nonempty

source

@[deprecated "lsub is deprecated" (since := "2026-03-27")]

theorem Ordinal.lsub_typein (o : Ordinal.{u}) :

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

source

@[deprecated Order.IsSuccPrelimit.sSup_Iio (since := "2026-03-27")]

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

source

@[deprecated csSup_Iic (since := "2026-03-27")]

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

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

source

@[deprecated "write `⨆ i : Iio o, f i + 1` instead." (since := "2026-03-23")]

noncomputable 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}.

Equations

o.blsub f = o.bsup fun (a : Ordinal.{?u.23}) (ha : a < o) => Order.succ (f a ha)

Instances For

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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_3}) :

lsub (familyOfBFamily' r ho f) = o.blsub f

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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)

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

(type r).blsub (bfamilyOfFamily' r f) = lsub f

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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)

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

theorem Ordinal.blsub_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) :

(type WellOrderingRel).blsub (bfamilyOfFamily f) = lsub f

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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 ⋯

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

theorem Ordinal.blsub_le {o : Ordinal.{u_3}} {f : (b : Ordinal.{u_3}) → b < o → Ordinal.{max u_3 u_4}} {a : Ordinal.{max u_3 u_4}} :

(∀ (i : Ordinal.{u_3}) (h : i < o), f i h < a) → o.blsub f ≤ a

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

f i h < o.blsub f

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

o.bsup f ≤ o.blsub f

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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)

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

theorem Ordinal.blsub_eq_zero_iff {o : Ordinal.{u_3}} {f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}} :

o.blsub f = 0 ↔ o = 0

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

blsub 0 f = 0

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

0 < o.blsub f

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

theorem Ordinal.blsub_one (f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}) :

blsub 1 f = Order.succ (f 0 ⋯)

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

theorem Ordinal.blsub_id (o : Ordinal.{u}) :

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

source

@[deprecated Order.IsSuccPrelimit.sSup_Iio (since := "2026-03-23")]

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

source

@[deprecated csSup_Iic (since := "2026-03-23")]

theorem Ordinal.bsup_id_add_one (o : Ordinal.{u}) :

((o + 1).bsup fun (x : Ordinal.{u}) (x_1 : x < o + 1) => x) = o

source

@[deprecated csSup_Iic (since := "2026-03-23")]

theorem Ordinal.bsup_id_succ (o : Ordinal.{u}) :

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated "blsub is deprecated" (since := "2026-03-23")]

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

source

@[deprecated Ordinal.IsNormal.apply_of_isSuccLimit (since := "2026-03-23")]

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

source

@[deprecated Ordinal.IsNormal.apply_of_isSuccLimit (since := "2026-03-23")]

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

source

@[deprecated Order.isNormal_iff (since := "2026-03-23")]

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

source

@[deprecated Order.isNormal_iff (since := "2026-03-23")]

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

source

@[deprecated Order.IsNormal.ext_iff (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 #

source

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

¬Function.Surjective f

source

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

¬Function.Injective f

source

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.

source

instance Ordinal.uncountable :

Uncountable Ordinal.{u}

source

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 #

source

@[simp]

theorem Ordinal.iSup_natCast :

iSup Nat.cast = omega0

source

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

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

source

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

source

@[simp]

theorem Ordinal.add_iSup (o : Ordinal.{u}) {ι : Type u_1} [Small.{u, u_1} ι] [Nonempty ι] (f : ι → Ordinal.{u}) :

o + ⨆ (i : ι), f i = ⨆ (i : ι), o + f i

source

@[simp]

theorem Ordinal.add_sSup (o : Ordinal.{u}) {s : Set Ordinal.{u}} [Small.{u, u + 1} ↑s] (hs : s.Nonempty) :

o + sSup s = sSup ((fun (x : Ordinal.{u}) => o + x) '' s)

source

@[simp]

theorem Ordinal.mul_sSup (o : Ordinal.{u_1}) (s : Set Ordinal.{u_1}) :

o * sSup s = sSup ((fun (x : Ordinal.{u_1}) => o * x) '' s)

source

@[simp]

theorem Ordinal.mul_iSup (o : Ordinal.{u_1}) {ι : Sort u_2} (f : ι → Ordinal.{u_1}) :

o * ⨆ (i : ι), f i = ⨆ (i : ι), o * f i

source

@[simp]

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

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

source

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

source

@[simp]

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

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

source

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

Documentation

Mathlib.SetTheory.Ordinal.Family

Arithmetic on families of ordinals #

Supremum of a family of ordinals #

Results about injectivity and surjectivity #

Casting naturals into ordinals, compatibility with operations #