Commit 2024-10-15 17:51 a4dc2792

View on Github →

refactor(SetTheory/Ordinal/Arithmetic): generalize universes of iSup theorems (#16996) Generalize the universes of iSup theorems.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

modified theorem Ordinal.iSup_eq_zero_iff

modified theorem Ordinal.iSup_sum

modified theorem Ordinal.succ_lt_iSup_of_ne_iSup

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/SetTheory/ZFC/Rank.lean