Set intervals in a successor-predecessor order #
This file proves relations between the various set intervals in a successor/predecessor order.
Notes #
Please keep in sync with:
Mathlib/Algebra/Order/Interval/Finset/SuccPred.leanMathlib/Algebra/Order/Interval/Set/SuccPred.leanMathlib/Order/Interval/Finset/SuccPred.lean
TODO #
Copy over insert lemmas from Mathlib/Order/Interval/Finset/Nat.lean.
Two-sided intervals #
theorem
Set.Ico_succ_left_eq_Ioo
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
(a b : α)
:
Ico (Order.succ a) b = Ioo a b
theorem
Set.Icc_succ_left_eq_Ioc_of_not_isMax
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a : α}
(ha : ¬IsMax a)
(b : α)
:
Icc (Order.succ a) b = Ioc a b
theorem
Set.Ico_succ_right_eq_Icc_of_not_isMax
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{b : α}
(hb : ¬IsMax b)
(a : α)
:
Ico a (Order.succ b) = Icc a b
theorem
Set.Ioo_succ_right_eq_Ioc_of_not_isMax
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{b : α}
(hb : ¬IsMax b)
(a : α)
:
Ioo a (Order.succ b) = Ioc a b
theorem
Set.Ico_succ_succ_eq_Ioc_of_not_isMax
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{b : α}
(hb : ¬IsMax b)
(a : α)
:
Ico (Order.succ a) (Order.succ b) = Ioc a b
Inserting into intervals #
theorem
Set.insert_Icc_succ_left_eq_Icc
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
(h : a ≤ b)
:
insert a (Icc (Order.succ a) b) = Icc a b
theorem
Set.insert_Icc_right_eq_Icc_succ
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
(h : a ≤ Order.succ b)
:
insert (Order.succ b) (Icc a b) = Icc a (Order.succ b)
theorem
Set.insert_Ico_right_eq_Ico_succ_of_not_isMax
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
(h : a ≤ b)
(hb : ¬IsMax b)
:
insert b (Ico a b) = Ico a (Order.succ b)
theorem
Set.insert_Ico_succ_left_eq_Ico
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
(h : a < b)
:
insert a (Ico (Order.succ a) b) = Ico a b
theorem
Set.insert_Ioc_right_eq_Ioc_succ_of_not_isMax
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
(h : a ≤ b)
(hb : ¬IsMax b)
:
insert (Order.succ b) (Ioc a b) = Ioc a (Order.succ b)
theorem
Set.insert_Ioc_succ_left_eq_Ioc
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
(h : a < b)
:
insert (Order.succ a) (Ioc (Order.succ a) b) = Ioc a b
theorem
Set.Icc_succ_left_eq_Ioc
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
[NoMaxOrder α]
(a b : α)
:
Icc (Order.succ a) b = Ioc a b
theorem
Set.Ico_succ_right_eq_Icc
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
[NoMaxOrder α]
(a b : α)
:
Ico a (Order.succ b) = Icc a b
theorem
Set.Ioo_succ_right_eq_Ioc
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
[NoMaxOrder α]
(a b : α)
:
Ioo a (Order.succ b) = Ioc a b
theorem
Set.Ico_succ_succ_eq_Ioc
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
[NoMaxOrder α]
(a b : α)
:
Ico (Order.succ a) (Order.succ b) = Ioc a b
Inserting into intervals #
theorem
Set.insert_Ico_right_eq_Ico_succ
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
(h : a ≤ b)
:
insert b (Ico a b) = Ico a (Order.succ b)
theorem
Set.insert_Ioc_right_eq_Ioc_succ
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
(h : a ≤ b)
:
insert (Order.succ b) (Ioc a b) = Ioc a (Order.succ b)
theorem
Set.Ioc_pred_right_eq_Ioo
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
(a b : α)
:
Ioc a (Order.pred b) = Ioo a b
theorem
Set.Icc_pred_right_eq_Ico_of_not_isMin
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{b : α}
(hb : ¬IsMin b)
(a : α)
:
Icc a (Order.pred b) = Ico a b
theorem
Set.Ioc_pred_left_eq_Icc_of_not_isMin
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a : α}
(ha : ¬IsMin a)
(b : α)
:
Ioc (Order.pred a) b = Icc a b
theorem
Set.Ioo_pred_left_eq_Ioc_of_not_isMin
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a : α}
(ha : ¬IsMin a)
(b : α)
:
Ioo (Order.pred a) b = Ico a b
theorem
Set.Ioc_pred_pred_eq_Ico_of_not_isMin
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a : α}
(ha : ¬IsMin a)
(b : α)
:
Ioc (Order.pred a) (Order.pred b) = Ico a b
Inserting into intervals #
theorem
Set.insert_Icc_pred_right_eq_Icc
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
(h : a ≤ b)
:
insert b (Icc a (Order.pred b)) = Icc a b
theorem
Set.insert_Icc_left_eq_Icc_pred
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
(h : Order.pred a ≤ b)
:
insert (Order.pred a) (Icc a b) = Icc (Order.pred a) b
theorem
Set.insert_Ioc_left_eq_Ioc_pred_of_not_isMin
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
(h : a ≤ b)
(ha : ¬IsMin a)
:
insert a (Ioc a b) = Ioc (Order.pred a) b
theorem
Set.insert_Ioc_pred_right_eq_Ioc
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
(h : a < b)
:
insert b (Ioc a (Order.pred b)) = Ioc a b
theorem
Set.insert_Ico_left_eq_Ico_pred_of_not_isMin
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
(h : a ≤ b)
(ha : ¬IsMin a)
:
insert (Order.pred a) (Ico a b) = Ico (Order.pred a) b
theorem
Set.insert_Ico_pred_right_eq_Ico
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
(h : a < b)
:
insert (Order.pred b) (Ico a (Order.pred b)) = Ico a b
theorem
Set.Icc_pred_right_eq_Ico
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
[NoMinOrder α]
(a b : α)
:
Icc a (Order.pred b) = Ico a b
theorem
Set.Ioc_pred_left_eq_Icc
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
[NoMinOrder α]
(a b : α)
:
Ioc (Order.pred a) b = Icc a b
theorem
Set.Ioo_pred_left_eq_Ioc
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
[NoMinOrder α]
(a b : α)
:
Ioo (Order.pred a) b = Ico a b
theorem
Set.Ioc_pred_pred_eq_Ico
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
[NoMinOrder α]
(a b : α)
:
Ioc (Order.pred a) (Order.pred b) = Ico a b
Inserting into intervals #
theorem
Set.insert_Ioc_left_eq_Ioc_pred
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
(h : a ≤ b)
:
insert a (Ioc a b) = Ioc (Order.pred a) b
theorem
Set.insert_Ico_left_eq_Ico_pred
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
(h : a ≤ b)
:
insert (Order.pred a) (Ico a b) = Ico (Order.pred a) b
theorem
Set.Icc_succ_pred_eq_Ioo
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
[PredOrder α]
[Nontrivial α]
(a b : α)
:
Icc (Order.succ a) (Order.pred b) = Ioo a b
One-sided interval towards ⊥ #
theorem
Set.Iio_succ_eq_Iic_of_not_isMax
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{b : α}
(hb : ¬IsMax b)
:
Iio (Order.succ b) = Iic b
theorem
Set.Iio_succ_eq_Iic
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
[NoMaxOrder α]
(b : α)
:
Iio (Order.succ b) = Iic b
theorem
Set.Iic_pred_eq_Iio_of_not_isMin
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{b : α}
(hb : ¬IsMin b)
:
Iic (Order.pred b) = Iio b
theorem
Set.Iic_pred_eq_Iio
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
[NoMinOrder α]
(b : α)
:
Iic (Order.pred b) = Iio b
One-sided interval towards ⊤ #
theorem
Set.Ici_succ_eq_Ioi_of_not_isMax
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a : α}
(ha : ¬IsMax a)
:
Ici (Order.succ a) = Ioi a
theorem
Set.Ici_succ_eq_Ioi
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
[NoMaxOrder α]
(a : α)
:
Ici (Order.succ a) = Ioi a
theorem
Set.Ioi_pred_eq_Ici_of_not_isMin
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a : α}
(ha : ¬IsMin a)
:
Ioi (Order.pred a) = Ici a
theorem
Set.Ioi_pred_eq_Ici
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
[NoMinOrder α]
(a : α)
:
Ioi (Order.pred a) = Ici a