Commit 2023-08-01 21:18 5f76a61b

View on Github →

feat: miscellaneous results about Filter.IsBoundedUnder (#6287)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Exp.lean

Modified Mathlib/Order/LiminfLimsup.lean

modified theorem Antitone.isBoundedUnder_ge_comp

added theorem Antitone.isBoundedUnder_ge_comp_iff

modified theorem Antitone.isBoundedUnder_le_comp

added theorem Antitone.isBoundedUnder_le_comp_iff

added theorem Filter.IsBoundedUnder.comp

added theorem Filter.IsBoundedUnder.isCoboundedUnder_flip

added theorem Filter.IsBoundedUnder.isCoboundedUnder_ge

added theorem Filter.IsBoundedUnder.isCoboundedUnder_le

modified theorem Monotone.isBoundedUnder_ge_comp

added theorem Monotone.isBoundedUnder_ge_comp_iff

modified theorem Monotone.isBoundedUnder_le_comp

added theorem Monotone.isBoundedUnder_le_comp_iff