Finset intervals in a successor-predecessor order

This file proves relations between the various finset intervals in a successor/predecessor order.

Notes

Please keep in sync with:

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

TODO

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

Two-sided intervals

theorem Finset.Ico_succ_left_eq_Ioo {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] (a b : α) : Ico (Order.succ a) b = Ioo a b

theorem Finset.Icc_succ_left_eq_Ioc_of_not_isMax {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a : α} (ha : ¬IsMax a) (b : α) : Icc (Order.succ a) b = Ioc a b

theorem Finset.Ico_succ_right_eq_Icc_of_not_isMax {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {b : α} (hb : ¬IsMax b) (a : α) : Ico a (Order.succ b) = Icc a b

theorem Finset.Ioo_succ_right_eq_Ioc_of_not_isMax {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {b : α} (hb : ¬IsMax b) (a : α) : Ioo a (Order.succ b) = Ioc a b

theorem Finset.Ico_succ_succ_eq_Ioc_of_not_isMax {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {b : α} (hb : ¬IsMax b) (a : α) : Ico (Order.succ a) (Order.succ b) = Ioc a b

theorem Finset.Icc_succ_left_eq_Ioc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Icc (Order.succ a) b = Ioc a b

theorem Finset.Ico_succ_right_eq_Icc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Ico a (Order.succ b) = Icc a b

theorem Finset.Ioo_succ_right_eq_Ioc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Ioo a (Order.succ b) = Ioc a b

theorem Finset.Ico_succ_succ_eq_Ioc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Ico (Order.succ a) (Order.succ b) = Ioc a b

theorem Finset.Ioc_pred_right_eq_Ioo {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] (a b : α) : Ioc a (Order.pred b) = Ioo a b

theorem Finset.Icc_pred_right_eq_Ico_of_not_isMin {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {b : α} (hb : ¬IsMin b) (a : α) : Icc a (Order.pred b) = Ico a b

theorem Finset.Ioc_pred_left_eq_Icc_of_not_isMin {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a : α} (ha : ¬IsMin a) (b : α) : Ioc (Order.pred a) b = Icc a b

theorem Finset.Ioo_pred_left_eq_Ioc_of_not_isMin {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a : α} (ha : ¬IsMin a) (b : α) : Ioo (Order.pred a) b = Ico a b

theorem Finset.Ioc_pred_pred_eq_Ico_of_not_isMin {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a : α} (ha : ¬IsMin a) (b : α) : Ioc (Order.pred a) (Order.pred b) = Ico a b

theorem Finset.Icc_pred_right_eq_Ico {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] [NoMinOrder α] (a b : α) : Icc a (Order.pred b) = Ico a b

theorem Finset.Ioc_pred_left_eq_Icc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] [NoMinOrder α] (a b : α) : Ioc (Order.pred a) b = Icc a b

theorem Finset.Ioo_pred_left_eq_Ioc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] [NoMinOrder α] (a b : α) : Ioo (Order.pred a) b = Ico a b

theorem Finset.Ioc_pred_pred_eq_Ico {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] [NoMinOrder α] (a b : α) : Ioc (Order.pred a) (Order.pred b) = Ico a b

theorem Finset.Icc_succ_pred_eq_Ioo {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [PredOrder α] [Nontrivial α] (a b : α) : Icc (Order.succ a) (Order.pred b) = Ioo a b

One-sided interval towards ⊥

theorem Finset.Iio_succ_eq_Iic_of_not_isMax {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] [SuccOrder α] {b : α} (hb : ¬IsMax b) : Iio (Order.succ b) = Iic b

theorem Finset.Iio_succ_eq_Iic {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] [SuccOrder α] [NoMaxOrder α] (b : α) : Iio (Order.succ b) = Iic b

theorem Finset.Iic_pred_eq_Iio_of_not_isMin {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] [PredOrder α] {b : α} (hb : ¬IsMin b) : Iic (Order.pred b) = Iio b

theorem Finset.Iic_pred_eq_Iio {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] [PredOrder α] [NoMinOrder α] (b : α) : Iic (Order.pred b) = Iio b

One-sided interval towards ⊤

theorem Finset.Ici_succ_eq_Ioi_of_not_isMax {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderTop α] [SuccOrder α] {a : α} (ha : ¬IsMax a) : Ici (Order.succ a) = Ioi a

theorem Finset.Ici_succ_eq_Ioi {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderTop α] [SuccOrder α] [NoMaxOrder α] (a : α) : Ici (Order.succ a) = Ioi a

theorem Finset.Ioi_pred_eq_Ici_of_not_isMin {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderTop α] [PredOrder α] {a : α} (ha : ¬IsMin a) : Ioi (Order.pred a) = Ici a

theorem Finset.Ioi_pred_eq_Ici {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderTop α] [PredOrder α] [NoMinOrder α] (a : α) : Ioi (Order.pred a) = Ici a