mathlib

0c844566 - feat(order,data/set/intervals): lemmas about `is_bot`/`is_top` (#11412)

feat(order,data/set/intervals): lemmas about `is_bot`/`is_top` (#11412) * add `is_top.Iic_eq`, `is_bot.Ici_eq`, `is_top.Ioi_eq`, `is_bot.Iio_eq`, `set.Ioi_top`, `set.Iio_bot`; * rename `set.Ici_singleton_of_top` and `set.Iic_singleton_of_bot` to `is_top.Ici_eq` and `is_bot.Iic_eq`; * add `is_top_or_exists_gt`, `is_bot_or_exists_lt`, `is_top_top`, and `is_bot_bot`; * add `is_top.to_dual` and `is_bot.to_dual`; * add `set.empty_ssubset`.