Theorems · Definition · logic and foundations

Ordinal.bsup

Deprecated since 2026-04-05Mathlib marks this declaration as deprecated.

(o : Ordinal.{u}) → ((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.

Defined in

Mathlib.SetTheory.Ordinal.Family

Cited by

49 results in Mathlib

Foundations

Depth 40 from the axioms · uses propext, Classical.choice, Quot.sound