Commit 2024-02-26 06:46 f13499e1

View on Github →

feat: isCoboundedUnder_le lemmas (#10946)

Estimated changes

Modified Mathlib/Order/LiminfLimsup.lean

added theorem Filter.isCoboundedUnder_ge_of_eventually_le

added theorem Filter.isCoboundedUnder_ge_of_le

added theorem Filter.isCoboundedUnder_le_of_eventually_le

added theorem Filter.isCoboundedUnder_le_of_le