mathlib3
9be829e9 - feat(order/bounds): add basic lemmas about bdd_below (#5186)

Commit
5 years ago
feat(order/bounds): add basic lemmas about bdd_below (#5186) Lemmas for bounded intervals (`Icc`, `Ico`, `Ioc` and `Ioo`). There were lemmas for `bdd_above` but the ones for `bdd_below` were missing.
Author
Parents
Loading