Commit 2025-08-22 21:50 5e955262

View on Github →

feat: Cardinal.ord is a normal function (#28752) We also generalize ord_sSup and ord_iSup (which didn't require the BddAbove argument).

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

added theorem Cardinal.bddAbove_ord_image_iff

added theorem Cardinal.isNormal_ord

Modified Mathlib/SetTheory/Ordinal/Family.lean

modified theorem Ordinal.iSup_ord

modified theorem Ordinal.sSup_ord