Commit 2024-07-21 18:30 9b782fff

View on Github →

feat: IsBoundedUnder lemmas for addition and Finset.sum (#13966)

Estimated changes

Modified Mathlib/Order/LiminfLimsup.lean

added theorem Filter.isBoundedUnder_ge_add

added theorem Filter.isBoundedUnder_ge_sum

added theorem Filter.isBoundedUnder_le_add

added theorem Filter.isBoundedUnder_le_sum

added theorem Filter.isBoundedUnder_sum