Commit 2024-09-14 08:36 aa90d83a

View on Github →

feat(Order/LiminfLimsup): reinstate lemmas (#16765)

Estimated changes

Modified Mathlib/Order/LiminfLimsup.lean

added theorem BddAbove.isBoundedUnder_of_range

added theorem BddBelow.isBoundedUnder_of_range