Theorem Ordinal.iSup_add_one_le

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.iSup_add_one_leView on Github →