Theorem Ordinal.add_iSup

Modification history

2026-04-05 08:48
Mathlib/SetTheory/Ordinal/Family.lean
feat(SetTheory/Ordinal): add `add_iSup`, `mul_iSup` and friends (#37470) …
Added Ordinal.add_iSupView on Github →