Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-13 07:08 0c844566

View on Github →

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.

Estimated changes

added theorem set.empty_ssubset
added theorem is_bot.Ici_eq
added theorem is_bot.Iic_eq
added theorem is_bot.Iio_eq
added theorem is_top.Ici_eq
added theorem is_top.Iic_eq
added theorem is_top.Ioi_eq
modified theorem set.Ici_bot
deleted theorem set.Ici_singleton_of_top
modified theorem set.Iic_inter_Ioc_of_le
deleted theorem set.Iic_singleton_of_bot
modified theorem set.Iic_top
added theorem set.Iio_bot
added theorem set.Ioi_top
added theorem is_bot_or_exists_lt
added theorem is_top_or_exists_gt
added theorem is_bot_bot
added theorem is_top_top
added theorem is_bot.to_dual
added theorem is_top.to_dual