Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-03 09:27 b681b6b9

View on Github →

chore(order/bounds): add @[simp] attrs, add not_bdd_*_univ (#8520)

Estimated changes

Modified src/order/bounds.lean

modified theorem no_bot_order.lower_bounds_univ

modified theorem no_top_order.upper_bounds_univ

added theorem not_bdd_above_univ

added theorem not_bdd_below_univ

modified theorem order_bot.lower_bounds_univ

modified theorem order_top.upper_bounds_univ