Theorem Filter.isBoundedUnder_iff_eventually_bddAbove

Modification history

2024-08-26 10:46
Mathlib/Order/LiminfLimsup.lean
feat: A function is eventually bounded above/below iff it's eventually `BddAbove`/`BddBelow` (#16117) …
Added Filter.isBoundedUnder_iff_eventually_bddAboveView on Github →