Theorem bddBelow_insert

Modification history

2023-09-13 10:00

Mathlib/Order/Bounds/Basic.lean

chore: Generalise and move liminf/limsup lemmas (#6846) …

Modified bddBelow_insert View on Github →

2022-12-15 21:06

Mathlib/Order/Bounds/Basic.lean

feat: port Order.Bounds.Basic (#1040) …

Added bddBelow_insert View on Github →