Commit 2024-10-22 17:45 bbab98c8

View on Github →

feat(SetTheory/Ordinal/Arithmetic): IsNormal.iSup (#16866) Prove IsNormal.iSup, the iSup version of IsNormal.sup.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/UnivLE.lean

added theorem Ordinal.univLE_of_injective

added theorem univLE_iff_exists_embedding

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.IsLimit.iSup_Iio

added theorem Ordinal.IsLimit.sSup_Iio

added theorem Ordinal.IsNormal.apply_of_isLimit

modified theorem Ordinal.IsNormal.map_iSup

added theorem Ordinal.IsNormal.map_iSup_of_bddAbove

added theorem Ordinal.IsNormal.map_sSup

added theorem Ordinal.IsNormal.map_sSup_of_bddAbove

added theorem Ordinal.bddAbove_image

added theorem Ordinal.bddAbove_range_comp