Theorem Ordinal.lt_iSup_add_one

Modification history

2026-03-27 12:01
Mathlib/SetTheory/Ordinal/Family.lean
feat(SetTheory/Ordinal): small lemmas on `⨆ i, f i + 1` (#37264) …
Added Ordinal.lt_iSup_add_oneView on Github →