Commit 2024-08-26 10:46 7156387f

View on Github →

feat: A function is eventually bounded above/below iff it's eventually BddAbove/BddBelow (#16117) Translate between two statements that are "obviously the same"

Estimated changes

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

Modified Mathlib/Order/LiminfLimsup.lean

modified theorem BddAbove.isBoundedUnder

modified theorem BddBelow.isBoundedUnder

added theorem Filter.isBoundedUnder_iff_eventually_bddAbove

added theorem Filter.isBoundedUnder_iff_eventually_bddBelow