Theorem Ordinal.iSup_eq_bsup

Modification history

2025-03-18 10:08

Mathlib/SetTheory/Ordinal/Arithmetic.lean

chore(SetTheory): split `Ordinal/Arithmetic.lean` (#23017) …

Modified Ordinal.iSup_eq_bsup View on Github →

2024-11-04 14:05

Mathlib/SetTheory/Ordinal/Arithmetic.lean

feat(SetTheory/Ordinal/FixedPoint): generalize universes of `nfpFamily` (#17751) …

Added Ordinal.iSup_eq_bsup View on Github →