Theorem Ordinal.IsFundamentalSeq.iSup_add_one_eq

Modification history

2026-03-25 04:37
Mathlib/SetTheory/Ordinal/FundamentalSequence.lean
feat(SetTheory/Ordinal): fundamental sequences (#37019) …
Added Ordinal.IsFundamentalSeq.iSup_add_one_eqView on Github →