Commit 2025-01-13 15:16 e9171f0a

View on Github →

feat(Algebra/Order/Ring/Unbundled/Nonneg.lean): add boundedness lemmas (#18172) Lemmas about limsup and bddAbove needed for #15373.

Estimated changes

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

added theorem MonotoneOn.mul

Modified Mathlib/Algebra/Order/Ring/Unbundled/Nonneg.lean

added theorem BddAbove.range_comp_of_nonneg

added theorem bddAbove_range_mul

Modified Mathlib/Order/LiminfLimsup.lean

added theorem Filter.eventually_add_neg_lt_of_le_liminf

added theorem Filter.eventually_lt_add_pos_of_limsup_le

added theorem Filter.exists_lt_of_le_liminf

added theorem Filter.exists_lt_of_limsup_le