Commit 2026-01-30 10:38 f4d4f2ad

View on Github →

feat(NNReal): supremum commutes with Nat.cast (#34467) as well as the infimum version, and some simple helper lemmas to get there.

Estimated changes

Modified Mathlib/Data/NNReal/Basic.lean

added theorem NNReal.bddAbove_natCast_image_iff

added theorem NNReal.bddAbove_range_natCast_iff

added theorem NNReal.natCast_iInf

added theorem NNReal.natCast_iSup

Modified Mathlib/Data/Nat/Lattice.lean

added theorem Nat.iSup_of_not_bddAbove