Documentation

Mathlib.Algebra.Order.Interval.Finset.SuccPred

Finset intervals in an additive successor-predecessor order #

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

Notes #

Please keep in sync with:

TODO #

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

Two-sided intervals #

Orders possibly with maximal elements #

Equalities of intervals #

theorem Finset.Ico_add_one_left_eq_Ioo {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] (a b : α) :

Ico (a + 1) b = Ioo a b

theorem Finset.Icc_add_one_left_eq_Ioc_of_not_isMax {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] {a : α} (ha : ¬IsMax a) (b : α) :

Icc (a + 1) b = Ioc a b

theorem Finset.Ico_add_one_right_eq_Icc_of_not_isMax {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] {b : α} (hb : ¬IsMax b) (a : α) :

Ico a (b + 1) = Icc a b

theorem Finset.Ioo_add_one_right_eq_Ioc_of_not_isMax {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] {b : α} (hb : ¬IsMax b) (a : α) :

Ioo a (b + 1) = Ioc a b

theorem Finset.Ico_add_one_add_one_eq_Ioc_of_not_isMax {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] {b : α} (hb : ¬IsMax b) (a : α) :

Ico (a + 1) (b + 1) = Ioc a b

Inserting into intervals #

theorem Finset.insert_Icc_add_one_left_eq_Icc {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] {a b : α} (h : a ≤ b) :

insert a (Icc (a + 1) b) = Icc a b

theorem Finset.insert_Icc_right_eq_Icc_add_one {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] {a b : α} (h : a ≤ b + 1) :

insert (b + 1) (Icc a b) = Icc a (b + 1)

theorem Finset.insert_Ico_right_eq_Ico_add_one_of_not_isMax {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] {a b : α} (h : a ≤ b) (hb : ¬IsMax b) :

insert b (Ico a b) = Ico a (b + 1)

theorem Finset.insert_Ico_add_one_left_eq_Ico {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] {a b : α} (h : a < b) :

insert a (Ico (a + 1) b) = Ico a b

theorem Finset.insert_Ioc_right_eq_Ioc_add_one_of_not_isMax {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] {a b : α} (h : a ≤ b) (hb : ¬IsMax b) :

insert (b + 1) (Ioc a b) = Ioc a (b + 1)

theorem Finset.insert_Ioc_add_one_left_eq_Ioc {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] {a b : α} (h : a < b) :

insert (a + 1) (Ioc (a + 1) b) = Ioc a b

Orders with no maximal elements #

Equalities of intervals #

theorem Finset.Icc_add_one_left_eq_Ioc {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α) :

Icc (a + 1) b = Ioc a b

theorem Finset.Ico_add_one_right_eq_Icc {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α) :

Ico a (b + 1) = Icc a b

theorem Finset.Ioo_add_one_right_eq_Ioc {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α) :

Ioo a (b + 1) = Ioc a b

theorem Finset.Ico_add_one_add_one_eq_Ioc {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α) :

Ico (a + 1) (b + 1) = Ioc a b

Inserting into intervals #

theorem Finset.insert_Ico_right_eq_Ico_add_one {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] {a b : α} [NoMaxOrder α] (h : a ≤ b) :

insert b (Ico a b) = Ico a (b + 1)

theorem Finset.insert_Ioc_right_eq_Ioc_add_one {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [SuccAddOrder α] {a b : α} [NoMaxOrder α] (h : a ≤ b) :

insert (b + 1) (Ioc a b) = Ioc a (b + 1)

Orders possibly with minimal elements #

Equalities of intervals #

theorem Finset.Ioc_sub_one_right_eq_Ioo {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] (a b : α) :

Ioc a (b - 1) = Ioo a b

theorem Finset.Icc_sub_one_right_eq_Ico_of_not_isMin {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {b : α} (hb : ¬IsMin b) (a : α) :

Icc a (b - 1) = Ico a b

theorem Finset.Ioc_sub_one_left_eq_Icc_of_not_isMin {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {a : α} (ha : ¬IsMin a) (b : α) :

Ioc (a - 1) b = Icc a b

theorem Finset.Ioo_sub_one_left_eq_Ico_of_not_isMin {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {a : α} (ha : ¬IsMin a) (b : α) :

Ioo (a - 1) b = Ico a b

@[deprecated Finset.Ioo_sub_one_left_eq_Ico_of_not_isMin (since := "2026-09-03")]

theorem Finset.Ioo_sub_one_left_eq_Ioc_of_not_isMin {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {a : α} (ha : ¬IsMin a) (b : α) :

Ioo (a - 1) b = Ico a b

Alias of Finset.Ioo_sub_one_left_eq_Ico_of_not_isMin.

theorem Finset.Ioc_sub_one_sub_one_eq_Ico_of_not_isMin {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {a : α} (ha : ¬IsMin a) (b : α) :

Ioc (a - 1) (b - 1) = Ico a b

Inserting into intervals #

theorem Finset.insert_Icc_sub_one_right_eq_Icc {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {a b : α} (h : a ≤ b) :

insert b (Icc a (b - 1)) = Icc a b

theorem Finset.insert_Icc_left_eq_Icc_sub_one {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {a b : α} (h : a - 1 ≤ b) :

insert (a - 1) (Icc a b) = Icc (a - 1) b

theorem Finset.insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {a b : α} (h : a ≤ b) (ha : ¬IsMin a) :

insert a (Ioc a b) = Ioc (a - 1) b

theorem Finset.insert_Ioc_sub_one_right_eq_Ioc {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {a b : α} (h : a < b) :

insert b (Ioc a (b - 1)) = Ioc a b

theorem Finset.insert_Ico_left_eq_Ico_sub_one_of_not_isMin {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {a b : α} (h : a ≤ b) (ha : ¬IsMin a) :

insert (a - 1) (Ico a b) = Ico (a - 1) b

theorem Finset.insert_Ico_sub_one_right_eq_Ico {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {a b : α} (h : a < b) :

insert (b - 1) (Ico a (b - 1)) = Ico a b

Orders with no minimal elements #

Equalities of intervals #

theorem Finset.Icc_sub_one_right_eq_Ico {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α) :

Icc a (b - 1) = Ico a b

theorem Finset.Ioc_sub_one_left_eq_Icc {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α) :

Ioc (a - 1) b = Icc a b

theorem Finset.Ioo_sub_one_left_eq_Ico {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α) :

Ioo (a - 1) b = Ico a b

@[deprecated Finset.Ioo_sub_one_left_eq_Ico (since := "2026-09-03")]

theorem Finset.Ioo_sub_one_left_eq_Ioc {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α) :

Ioo (a - 1) b = Ico a b

Alias of Finset.Ioo_sub_one_left_eq_Ico.

theorem Finset.Ioc_sub_one_sub_one_eq_Ico {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α) :

Ioc (a - 1) (b - 1) = Ico a b

Inserting into intervals #

theorem Finset.insert_Ioc_left_eq_Ioc_sub_one {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {a b : α} [NoMinOrder α] (h : a ≤ b) :

insert a (Ioc a b) = Ioc (a - 1) b

theorem Finset.insert_Ico_left_eq_Ico_sub_one {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Sub α] [PredSubOrder α] {a b : α} [NoMinOrder α] (h : a ≤ b) :

insert (a - 1) (Ico a b) = Ico (a - 1) b

theorem Finset.Icc_add_one_sub_one_eq_Ioo {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrder α] [Add α] [Sub α] [SuccAddOrder α] [PredSubOrder α] [Nontrivial α] (a b : α) :

Icc (a + 1) (b - 1) = Ioo a b

One-sided interval towards `⊥` #

theorem Finset.Iio_add_one_eq_Iic_of_not_isMax {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrderBot α] [Add α] [SuccAddOrder α] {b : α} (hb : ¬IsMax b) :

Iio (b + 1) = Iic b

theorem Finset.Iio_add_one_eq_Iic {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrderBot α] [Add α] [SuccAddOrder α] [NoMaxOrder α] (b : α) :

Iio (b + 1) = Iic b

theorem Finset.Iic_sub_one_eq_Iio_of_not_isMin {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrderBot α] [Sub α] [PredSubOrder α] {b : α} (hb : ¬IsMin b) :

Iic (b - 1) = Iio b

theorem Finset.Iic_sub_one_eq_Iio {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrderBot α] [Sub α] [PredSubOrder α] [NoMinOrder α] (b : α) :

Iic (b - 1) = Iio b

One-sided interval towards `⊤` #

theorem Finset.Ici_add_one_eq_Ioi_of_not_isMax {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrderTop α] [Add α] [SuccAddOrder α] {a : α} (ha : ¬IsMax a) :

Ici (a + 1) = Ioi a

theorem Finset.Ici_add_one_eq_Ioi {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrderTop α] [Add α] [SuccAddOrder α] [NoMaxOrder α] (a : α) :

Ici (a + 1) = Ioi a

theorem Finset.Ioi_sub_one_eq_Ici_of_not_isMin {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrderTop α] [Sub α] [PredSubOrder α] {a : α} (ha : ¬IsMin a) :

Ioi (a - 1) = Ici a

theorem Finset.Ioi_sub_one_eq_Ici {α : Type u_1} [LinearOrder α] [One α] [LocallyFiniteOrderTop α] [Sub α] [PredSubOrder α] [NoMinOrder α] (a : α) :

Ioi (a - 1) = Ici a