Documentation

Mathlib.Order.Interval.Finset.SuccPred

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:

TODO #

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

Two-sided intervals #

Orders possibly with maximal elements #

Equalities of intervals #
source
theorem Finset.Ico_succ_left_eq_Ioo {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] (a b : α) :
Ico (Order.succ a) b = Ioo a b
source
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
source
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
source
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
source
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
Inserting into intervals #
source
theorem Finset.insert_Icc_succ_left_eq_Icc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a ≤ b) :
insert a (Icc (Order.succ a) b) = Icc a b
source
theorem Finset.insert_Icc_right_eq_Icc_succ {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a ≤ Order.succ b) :
insert (Order.succ b) (Icc a b) = Icc a (Order.succ b)
source
@[deprecated Finset.insert_Icc_right_eq_Icc_succ (since := "2025-04-19")]
theorem Finset.insert_Icc_eq_Icc_succ_right {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a ≤ Order.succ b) :
insert (Order.succ b) (Icc a b) = Icc a (Order.succ b)

Alias of Finset.insert_Icc_right_eq_Icc_succ.

source
theorem Finset.insert_Ico_right_eq_Ico_succ_of_not_isMax {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a ≤ b) (hb : ¬IsMax b) :
insert b (Ico a b) = Ico a (Order.succ b)
source
@[deprecated Finset.insert_Ico_right_eq_Ico_succ_of_not_isMax (since := "2025-04-14")]
theorem Finset.insert_Ico_right_eq_Ico_succ_right_of_not_isMax {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a ≤ b) (hb : ¬IsMax b) :
insert b (Ico a b) = Ico a (Order.succ b)

Alias of Finset.insert_Ico_right_eq_Ico_succ_of_not_isMax.

source
theorem Finset.insert_Ico_succ_left_eq_Ico {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a < b) :
insert a (Ico (Order.succ a) b) = Ico a b
source
theorem Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a ≤ b) (hb : ¬IsMax b) :
insert (Order.succ b) (Ioc a b) = Ioc a (Order.succ b)
source
theorem Finset.insert_Ioc_succ_left_eq_Ioc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a < b) :
insert (Order.succ a) (Ioc (Order.succ a) b) = Ioc a b

Orders with no maximal elements #

Equalities of intervals #
source
theorem Finset.Icc_succ_left_eq_Ioc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) :
Icc (Order.succ a) b = Ioc a b
source
theorem Finset.Ico_succ_right_eq_Icc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) :
Ico a (Order.succ b) = Icc a b
source
theorem Finset.Ioo_succ_right_eq_Ioc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) :
Ioo a (Order.succ b) = Ioc a b
source
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
Inserting into intervals #
source
theorem Finset.insert_Ico_right_eq_Ico_succ {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (h : a ≤ b) :
insert b (Ico a b) = Ico a (Order.succ b)
source
@[deprecated Finset.insert_Ico_right_eq_Ico_succ (since := "2025-04-14")]
theorem Finset.insert_Ico_right_eq_Ico_succ_right {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (h : a ≤ b) :
insert b (Ico a b) = Ico a (Order.succ b)

Alias of Finset.insert_Ico_right_eq_Ico_succ.

source
theorem Finset.insert_Ioc_right_eq_Ioc_succ {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (h : a ≤ b) :
insert (Order.succ b) (Ioc a b) = Ioc a (Order.succ b)

Orders possibly with minimal elements #

Equalities of intervals #
source
theorem Finset.Ioc_pred_right_eq_Ioo {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] (a b : α) :
Ioc a (Order.pred b) = Ioo a b
source
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
source
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
source
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
source
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
Inserting into intervals #
source
theorem Finset.insert_Icc_pred_right_eq_Icc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a b : α} (h : a ≤ b) :
insert b (Icc a (Order.pred b)) = Icc a b
source
theorem Finset.insert_Icc_left_eq_Icc_pred {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a b : α} (h : Order.pred a ≤ b) :
insert (Order.pred a) (Icc a b) = Icc (Order.pred a) b
source
@[deprecated Finset.insert_Icc_left_eq_Icc_pred (since := "2025-04-19")]
theorem Finset.insert_Icc_eq_Icc_pred_left {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a b : α} (h : Order.pred a ≤ b) :
insert (Order.pred a) (Icc a b) = Icc (Order.pred a) b

Alias of Finset.insert_Icc_left_eq_Icc_pred.

source
theorem Finset.insert_Ioc_left_eq_Ioc_pred_of_not_isMin {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a b : α} (h : a ≤ b) (ha : ¬IsMin a) :
insert a (Ioc a b) = Ioc (Order.pred a) b
source
@[deprecated Finset.insert_Ioc_left_eq_Ioc_pred_of_not_isMin (since := "2025-04-14")]
theorem Finset.insert_Ioc_left_eq_Ioc_pred_left_of_not_isMin {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a b : α} (h : a ≤ b) (ha : ¬IsMin a) :
insert a (Ioc a b) = Ioc (Order.pred a) b

Alias of Finset.insert_Ioc_left_eq_Ioc_pred_of_not_isMin.

source
theorem Finset.insert_Ioc_pred_right_eq_Ioc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a b : α} (h : a < b) :
insert b (Ioc a (Order.pred b)) = Ioc a b
source
theorem Finset.insert_Ico_left_eq_Ico_pred_of_not_isMin {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a b : α} (h : a ≤ b) (ha : ¬IsMin a) :
insert (Order.pred a) (Ico a b) = Ico (Order.pred a) b
source
theorem Finset.insert_Ico_pred_right_eq_Ico {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a b : α} (h : a < b) :
insert (Order.pred b) (Ico a (Order.pred b)) = Ico a b

Orders with no minimal elements #

Equalities of intervals #
source
theorem Finset.Icc_pred_right_eq_Ico {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] [NoMinOrder α] (a b : α) :
Icc a (Order.pred b) = Ico a b
source
theorem Finset.Ioc_pred_left_eq_Icc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] [NoMinOrder α] (a b : α) :
Ioc (Order.pred a) b = Icc a b
source
theorem Finset.Ioo_pred_left_eq_Ioc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] [NoMinOrder α] (a b : α) :
Ioo (Order.pred a) b = Ico a b
source
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
Inserting into intervals #
source
theorem Finset.insert_Ioc_left_eq_Ioc_pred {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a b : α} [NoMinOrder α] (h : a ≤ b) :
insert a (Ioc a b) = Ioc (Order.pred a) b
source
@[deprecated Finset.insert_Ioc_left_eq_Ioc_pred (since := "2025-04-14")]
theorem Finset.insert_Ioc_left_eq_Ioc_pred_left {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a b : α} [NoMinOrder α] (h : a ≤ b) :
insert a (Ioc a b) = Ioc (Order.pred a) b

Alias of Finset.insert_Ioc_left_eq_Ioc_pred.

source
theorem Finset.insert_Ico_left_eq_Ico_pred {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [PredOrder α] {a b : α} [NoMinOrder α] (h : a ≤ b) :
insert (Order.pred a) (Ico a b) = Ico (Order.pred a) b
source
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 ⊥ #

source
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
source
theorem Finset.Iio_succ_eq_Iic {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] [SuccOrder α] [NoMaxOrder α] (b : α) :
Iio (Order.succ b) = Iic b
source
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
source
theorem Finset.Iic_pred_eq_Iio {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] [PredOrder α] [NoMinOrder α] (b : α) :
Iic (Order.pred b) = Iio b

One-sided interval towards ⊤ #

source
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
source
theorem Finset.Ici_succ_eq_Ioi {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderTop α] [SuccOrder α] [NoMaxOrder α] (a : α) :
Ici (Order.succ a) = Ioi a
source
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
source
theorem Finset.Ioi_pred_eq_Ici {α : Type u_1} [LinearOrder α] [LocallyFiniteOrderTop α] [PredOrder α] [NoMinOrder α] (a : α) :
Ioi (Order.pred a) = Ici a