Set intervals in an additive successor-predecessor order

This file proves relations between the various set intervals in an additive successor/predecessor order.

Notes

Please keep in sync with:

• Mathlib.Algebra.Order.Interval.Finset.SuccPred
• Mathlib.Order.Interval.Finset.SuccPred
• Mathlib.Order.Interval.Set.SuccPred

TODO

Copy over insert lemmas from Mathlib.Order.Interval.Finset.Nat.

Two-sided intervals

theorem Set.Ico_add_one_left_eq_Ioo {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] (a b : α) : Ico (a + 1) b = Ioo a b

theorem Set.Icc_add_one_left_eq_Ioc_of_not_isMax {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] {a : α} (ha : ¬IsMax a) (b : α) : Icc (a + 1) b = Ioc a b

theorem Set.Ico_add_one_right_eq_Icc_of_not_isMax {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] {b : α} (hb : ¬IsMax b) (a : α) : Ico a (b + 1) = Icc a b

theorem Set.Ioo_add_one_right_eq_Ioc_of_not_isMax {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] {b : α} (hb : ¬IsMax b) (a : α) : Ioo a (b + 1) = Ioc a b

theorem Set.Ico_add_one_add_one_eq_Ioc_of_not_isMax {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] {b : α} (hb : ¬IsMax b) (a : α) : Ico (a + 1) (b + 1) = Ioc a b

theorem Set.Icc_add_one_left_eq_Ioc {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α) : Icc (a + 1) b = Ioc a b

theorem Set.Ico_add_one_right_eq_Icc {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α) : Ico a (b + 1) = Icc a b

theorem Set.Ioo_add_one_right_eq_Ioc {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α) : Ioo a (b + 1) = Ioc a b

theorem Set.Ico_add_one_add_one_eq_Ioc {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α) : Ico (a + 1) (b + 1) = Ioc a b

theorem Set.Ioc_sub_one_right_eq_Ioo {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] (a b : α) : Ioc a (b - 1) = Ioo a b

theorem Set.Icc_sub_one_right_eq_Ico_of_not_isMin {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] {b : α} (hb : ¬IsMin b) (a : α) : Icc a (b - 1) = Ico a b

theorem Set.Ioc_sub_one_left_eq_Icc_of_not_isMin {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] {a : α} (ha : ¬IsMin a) (b : α) : Ioc (a - 1) b = Icc a b

theorem Set.Ioo_sub_one_left_eq_Ioc_of_not_isMin {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] {a : α} (ha : ¬IsMin a) (b : α) : Ioo (a - 1) b = Ico a b

theorem Set.Ioc_sub_one_sub_one_eq_Ico_of_not_isMin {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] {a : α} (ha : ¬IsMin a) (b : α) : Ioc (a - 1) (b - 1) = Ico a b

theorem Set.Icc_sub_one_right_eq_Ico {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α) : Icc a (b - 1) = Ico a b

theorem Set.Ioc_sub_one_left_eq_Icc {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α) : Ioc (a - 1) b = Icc a b

theorem Set.Ioo_sub_one_left_eq_Ioc {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α) : Ioo (a - 1) b = Ico a b

theorem Set.Ioc_sub_one_sub_one_eq_Ico {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α) : Ioc (a - 1) (b - 1) = Ico a b

theorem Set.Icc_add_one_sub_one_eq_Ioo {α : Type u_2} [LinearOrder α] [One α] [Add α] [Sub α] [SuccAddOrder α] [PredSubOrder α] [Nontrivial α] (a b : α) : Icc (a + 1) (b - 1) = Ioo a b

One-sided interval towards ⊥

theorem Set.Iio_add_one_eq_Iic_of_not_isMax {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] {b : α} (hb : ¬IsMax b) : Iio (b + 1) = Iic b

theorem Set.Iio_add_one_eq_Iic {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] [NoMaxOrder α] (b : α) : Iio (b + 1) = Iic b

theorem Set.Iic_sub_one_eq_Iio_of_not_isMin {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] {b : α} (hb : ¬IsMin b) : Iic (b - 1) = Iio b

theorem Set.Iic_sub_one_eq_Iio {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] [NoMinOrder α] (b : α) : Iic (b - 1) = Iio b

One-sided interval towards ⊤

theorem Set.Ici_add_one_eq_Ioi_of_not_isMax {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] {a : α} (ha : ¬IsMax a) : Ici (a + 1) = Ioi a

theorem Set.Ici_add_one_eq_Ioi {α : Type u_2} [LinearOrder α] [One α] [Add α] [SuccAddOrder α] [NoMaxOrder α] (a : α) : Ici (a + 1) = Ioi a

theorem Set.Ioi_sub_one_eq_Ici_of_not_isMin {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] {a : α} (ha : ¬IsMin a) : Ioi (a - 1) = Ici a

theorem Set.Ioi_sub_one_eq_Ici {α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] [NoMinOrder α] (a : α) : Ioi (a - 1) = Ici a