Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-18 09:14 8d5caba3

View on Github →

chore(order/bounded_order): golf (#11538)

Estimated changes

modified theorem bot_lt_iff_ne_bot
modified theorem bot_unique
modified theorem eq_bot_iff
modified theorem eq_bot_mono
modified theorem eq_bot_of_minimal
modified theorem eq_bot_or_bot_lt
modified theorem eq_top_iff
modified theorem eq_top_mono
modified theorem eq_top_or_lt_top
modified theorem le_bot_iff
modified theorem ne_bot_of_gt
modified theorem ne_bot_of_le_ne_bot
modified theorem ne_top_of_le_ne_top
modified theorem ne_top_of_lt
modified theorem top_le_iff
modified theorem top_unique