Commit 2026-04-05 08:48 5a1c5fc6

View on Github →

feat(SetTheory/Ordinal): add add_iSup, mul_iSup and friends (#37470) Add a couple lemmas for working with ordinal iSup and sSup, addition and multiplication.

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

added theorem ciSup_bot

Modified Mathlib/SetTheory/Ordinal/Family.lean

added theorem Ordinal.add_iSup

added theorem Ordinal.add_sSup

modified theorem Ordinal.iSup_add_natCast

added theorem Ordinal.mul_iSup

added theorem Ordinal.mul_sSup