Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-31 12:36 45cfb254

View on Github →

refactor(order/bounded_order): Use is_min/is_max (#11408) Golf order.bounded_order and data.set.basic using is_min/is_max.

Estimated changes

modified theorem set.subsingleton_is_bot
modified theorem set.subsingleton_is_top
deleted theorem is_bot.Iic_eq
deleted theorem is_bot.Iio_eq
added theorem is_max.Ici_eq
added theorem is_max.Ioi_eq
added theorem is_min.Iic_eq
added theorem is_min.Iio_eq
deleted theorem is_top.Ici_eq
deleted theorem is_top.Ioi_eq
modified theorem set.Ici_top
modified theorem set.Iic_bot
modified theorem set.Iio_bot
modified theorem set.Ioi_top
added theorem eq_or_gt_of_le
modified theorem bot_le
added theorem bot_lt_top
modified theorem eq_bot_or_bot_lt
modified theorem is_bot_bot
modified theorem is_bot_iff_eq_bot
added theorem is_max_iff_eq_top
added theorem is_max_top
added theorem is_min_bot
added theorem is_min_iff_eq_bot
modified theorem is_top_iff_eq_top
modified theorem is_top_top
modified theorem le_top
modified theorem not_lt_bot
modified theorem not_top_lt
modified theorem top_ne_bot
deleted theorem is_bot.unique
deleted theorem is_top.unique