Commit 2026-07-01 14:49 8405ede1

View on Github →

feat(Order/Cover): intervals equal singletons iff (#37722) To complement Set.Icc_eq_singleton_iff, this introduces:

  • Set.Ioc_eq_singleton_iff / Set.Ico_eq_singleton_iff
  • Set.Ico_eq_singleton_left_iff / Set.Ioc_eq_singleton_right_iff
  • Set.Ioi_eq_singleton_iff / Set.Iio_eq_singleton_iff
  • Set.Ioi_eq_singleton_top_iff / Set.Iio_eq_singleton_bot_iff
  • Set.Ioo_eq_singleton_iff

Estimated changes