Successor and predecessor #
This file defines successor and predecessor orders. succ a, the successor of an element a : α is
the least element greater than a. pred a is the greatest element less than a. Typical examples
include ℕ, ℤ, ℕ+, Fin n, but also ENat, the lexicographic order of a successor/predecessor
order...
Typeclasses #
SuccOrder: Order equipped with a sensible successor function.PredOrder: Order equipped with a sensible predecessor function.
Implementation notes #
Maximal elements don't have a sensible successor. Thus the naïve typeclass
class NaiveSuccOrder (α : Type*) [Preorder α] where
(succ : α → α)
(succ_le_iff : ∀ {a b}, succ a ≤ b ↔ a < b)
(lt_succ_iff : ∀ {a b}, a < succ b ↔ a ≤ b)
can't apply to an OrderTop because plugging in a = b = ⊤ into either of succ_le_iff and
lt_succ_iff yields ⊤ < ⊤ (or more generally m < m for a maximal element m).
The solution taken here is to remove the implications ≤ → < and instead require that a < succ a
for all non maximal elements (enforced by the combination of le_succ and the contrapositive of
max_of_succ_le).
The stricter condition of every element having a sensible successor can be obtained through the
combination of SuccOrder α and NoMaxOrder α.
Equations
- instPredOrderOrderDualOfSuccOrder = { pred := ⇑OrderDual.toDual ∘ SuccOrder.succ ∘ ⇑OrderDual.ofDual, pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
Equations
- instSuccOrderOrderDualOfPredOrder = { succ := ⇑OrderDual.toDual ∘ PredOrder.pred ∘ ⇑OrderDual.ofDual, le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
def
SuccOrder.ofSuccLeIff
{α : Type u_1}
[Preorder α]
(succ : α → α)
(hsucc_le_iff : ∀ {a b : α}, succ a ≤ b ↔ a < b)
:
A constructor for SuccOrder α usable when α has no maximal element.
Equations
- SuccOrder.ofSuccLeIff succ hsucc_le_iff = { succ := succ, le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
def
PredOrder.ofLePredIff
{α : Type u_1}
[Preorder α]
(pred : α → α)
(hle_pred_iff : ∀ {a b : α}, a ≤ pred b ↔ a < b)
:
A constructor for PredOrder α usable when α has no minimal element.
Equations
- PredOrder.ofLePredIff pred hle_pred_iff = { pred := pred, pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
def
SuccOrder.ofCore
{α : Type u_1}
[LinearOrder α]
(succ : α → α)
(hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b)
(hm : ∀ (a : α), IsMax a → succ a = a)
:
A constructor for SuccOrder α for α a linear order.
Equations
- SuccOrder.ofCore succ hn hm = { succ := succ, le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
@[simp]
theorem
SuccOrder.ofCore_succ
{α : Type u_1}
[LinearOrder α]
(succ : α → α)
(hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b)
(hm : ∀ (a : α), IsMax a → succ a = a)
(a✝ : α)
:
def
PredOrder.ofCore
{α : Type u_1}
[LinearOrder α]
(pred : α → α)
(hn : ∀ {a : α}, ¬IsMin a → ∀ (b : α), b ≤ pred a ↔ b < a)
(hm : ∀ (a : α), IsMin a → pred a = a)
:
A constructor for PredOrder α for α a linear order.
Equations
- PredOrder.ofCore pred hn hm = { pred := pred, pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
@[simp]
theorem
PredOrder.ofCore_pred
{α : Type u_1}
[LinearOrder α]
(pred : α → α)
(hn : ∀ {a : α}, ¬IsMin a → ∀ (b : α), b ≤ pred a ↔ b < a)
(hm : ∀ (a : α), IsMin a → pred a = a)
(a✝ : α)
:
noncomputable def
SuccOrder.ofLinearWellFoundedLT
(α : Type u_1)
[LinearOrder α]
[WellFoundedLT α]
:
A well-order is a SuccOrder.
Equations
- SuccOrder.ofLinearWellFoundedLT α = SuccOrder.ofCore (fun (a : α) => if h : (Set.Ioi a).Nonempty then ⋯.min (Set.Ioi a) h else a) ⋯ ⋯
noncomputable def
PredOrder.ofLinearWellFoundedGT
(α : Type u_3)
[LinearOrder α]
[WellFoundedGT α]
:
A linear order with well-founded greater-than relation is a PredOrder.
Equations
Successor order #
Alias of Order.succ_le_of_lt.
theorem
IsMax.of_succ_le
{α : Type u_1}
[Preorder α]
[SuccOrder α]
{a : α}
:
Order.succ a ≤ a → IsMax a
Alias of the forward direction of Order.succ_le_iff_isMax.
Alias of the reverse direction of Order.succ_le_iff_isMax.
Alias of the reverse direction of Order.lt_succ_iff_not_isMax.
See also Order.succ_eq_of_covBy.
Alias of Order.le_succ_of_wcovBy.
See also Order.succ_eq_of_covBy.
@[simp]
@[simp]
theorem
Order.succ_lt_succ
{α : Type u_1}
[Preorder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
(hab : a < b)
:
theorem
Order.Iic_subset_Iio_succ
{α : Type u_1}
[Preorder α]
[SuccOrder α]
[NoMaxOrder α]
(a : α)
:
@[simp]
@[simp]
theorem
Order.Icc_subset_Ico_succ_right
{α : Type u_1}
[Preorder α]
[SuccOrder α]
[NoMaxOrder α]
(a b : α)
:
@[simp]
theorem
Order.Ioc_subset_Ioo_succ_right
{α : Type u_1}
[Preorder α]
[SuccOrder α]
[NoMaxOrder α]
(a b : α)
:
@[simp]
@[simp]
@[simp]
theorem
IsMax.succ_eq
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
:
IsMax a → Order.succ a = a
Alias of the reverse direction of Order.succ_eq_iff_isMax.
theorem
Order.succ_eq_of_covBy
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a b : α}
(h : a ⋖ b)
:
See also Order.le_succ_of_wcovBy.
Alias of Order.succ_eq_of_covBy.
See also Order.le_succ_of_wcovBy.
theorem
OrderIso.map_succ
{α : Type u_1}
{β : Type u_2}
[PartialOrder α]
[SuccOrder α]
[PartialOrder β]
[SuccOrder β]
(f : α ≃o β)
(a : α)
:
theorem
Order.succ_eq_iff_covBy
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
:
@[simp]
theorem
Order.bot_lt_succ
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
[OrderBot α]
[Nontrivial α]
(a : α)
:
theorem
Order.succ_ne_bot
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
[OrderBot α]
[Nontrivial α]
(a : α)
:
@[simp]
theorem
Order.succ_le_succ_iff
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
:
theorem
Order.succ_lt_succ_iff
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
:
theorem
Order.le_of_succ_le_succ
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
:
Alias of the forward direction of Order.succ_le_succ_iff.
theorem
Order.lt_of_succ_lt_succ
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
:
Alias of the forward direction of Order.succ_lt_succ_iff.
@[simp]
@[simp]
theorem
Order.Ico_succ_right
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
[NoMaxOrder α]
(a b : α)
:
@[simp]
theorem
Order.Ioo_succ_right
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
[NoMaxOrder α]
(a b : α)
:
@[simp]
theorem
Order.succ_eq_succ_iff
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
:
theorem
Order.succ_ne_succ_iff
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
:
Alias of the reverse direction of Order.succ_ne_succ_iff.
theorem
Order.lt_succ_iff_eq_or_lt
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
:
theorem
Order.Iio_succ_eq_insert
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
[NoMaxOrder α]
(a : α)
:
theorem
Order.Ico_succ_right_eq_insert
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
(h : a ≤ b)
:
theorem
Order.Ioo_succ_right_eq_insert
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
(h : a < b)
:
@[simp]
theorem
Order.Ioo_eq_empty_iff_le_succ
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a b : α}
[NoMaxOrder α]
:
theorem
Order.lt_succ_bot_iff
{α : Type u_1}
[LinearOrder α]
[SuccOrder α]
{a : α}
[OrderBot α]
[NoMaxOrder α]
:
There is at most one way to define the successors in a PartialOrder.
theorem
Order.succ_eq_csInf
{α : Type u_1}
[ConditionallyCompleteLattice α]
[SuccOrder α]
[NoMaxOrder α]
(a : α)
:
Predecessor order #
Alias of Order.le_pred_of_lt.
theorem
IsMin.of_le_pred
{α : Type u_1}
[Preorder α]
[PredOrder α]
{a : α}
:
a ≤ Order.pred a → IsMin a
Alias of the forward direction of Order.le_pred_iff_isMin.
Alias of the reverse direction of Order.le_pred_iff_isMin.
Alias of the reverse direction of Order.pred_lt_iff_not_isMin.
See also Order.pred_eq_of_covBy.
Alias of Order.pred_le_of_wcovBy.
See also Order.pred_eq_of_covBy.
@[simp]
@[simp]
theorem
Order.pred_le_pred_of_le
{α : Type u_1}
[Preorder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
:
theorem
Order.Ici_subset_Ioi_pred
{α : Type u_1}
[Preorder α]
[PredOrder α]
[NoMinOrder α]
(a : α)
:
@[simp]
@[simp]
theorem
Order.Icc_subset_Ioc_pred_left
{α : Type u_1}
[Preorder α]
[PredOrder α]
[NoMinOrder α]
(a b : α)
:
@[simp]
theorem
Order.Ico_subset_Ioo_pred_left
{α : Type u_1}
[Preorder α]
[PredOrder α]
[NoMinOrder α]
(a b : α)
:
@[simp]
@[simp]
@[simp]
theorem
IsMin.pred_eq
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
:
IsMin a → Order.pred a = a
Alias of the reverse direction of Order.pred_eq_iff_isMin.
theorem
Order.pred_eq_of_covBy
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a b : α}
(h : a ⋖ b)
:
See also Order.pred_le_of_wcovBy.
Alias of Order.pred_eq_of_covBy.
See also Order.pred_le_of_wcovBy.
theorem
OrderIso.map_pred
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{β : Type u_3}
[PartialOrder β]
[PredOrder β]
(f : α ≃o β)
(a : α)
:
theorem
Order.pred_eq_iff_covBy
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
:
@[simp]
theorem
Order.pred_lt_top
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
[OrderTop α]
[Nontrivial α]
(a : α)
:
theorem
Order.pred_ne_top
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
[OrderTop α]
[Nontrivial α]
(a : α)
:
@[simp]
theorem
Order.pred_le_pred_iff
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
:
theorem
Order.pred_lt_pred_iff
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
:
theorem
Order.le_of_pred_le_pred
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
:
Alias of the forward direction of Order.pred_le_pred_iff.
theorem
Order.lt_of_pred_lt_pred
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
:
Alias of the forward direction of Order.pred_lt_pred_iff.
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Order.pred_eq_pred_iff
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
:
theorem
Order.pred_ne_pred_iff
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
:
Alias of the reverse direction of Order.pred_ne_pred_iff.
theorem
Order.pred_lt_iff_eq_or_lt
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
:
theorem
Order.Ioi_pred_eq_insert
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
[NoMinOrder α]
(a : α)
:
theorem
Order.Ico_pred_right_eq_insert
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
(h : a ≤ b)
:
theorem
Order.Ioo_pred_right_eq_insert
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
(h : a < b)
:
@[simp]
theorem
Order.Ioo_eq_empty_iff_pred_le
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a b : α}
[NoMinOrder α]
:
theorem
Order.pred_top_lt_iff
{α : Type u_1}
[LinearOrder α]
[PredOrder α]
{a : α}
[OrderTop α]
[NoMinOrder α]
:
There is at most one way to define the predecessors in a PartialOrder.
theorem
Order.pred_eq_csSup
{α : Type u_1}
[ConditionallyCompleteLattice α]
[PredOrder α]
[NoMinOrder α]
(a : α)
:
Successor-predecessor orders #
theorem
Order.succ_pred
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
[PredOrder α]
[NoMinOrder α]
(a : α)
:
theorem
Order.pred_succ
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
[PredOrder α]
[NoMaxOrder α]
(a : α)
:
WithBot, WithTop #
Adding a greatest/least element to a SuccOrder or to a PredOrder.
As far as successors and predecessors are concerned, there are four ways to add a bottom or top element to an order:
- Adding a
⊤to anOrderTop: Preservessuccandpred. - Adding a
⊤to aNoMaxOrder: Preservessucc. Never preservespred. - Adding a
⊥to anOrderBot: Preservessuccandpred. - Adding a
⊥to aNoMinOrder: Preservespred. Never preservessucc. where "preserves(succ/pred)" means(Succ/Pred)Order α → (Succ/Pred)Order ((WithTop/WithBot) α).
instance
WithTop.instSuccOrder
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
[(a : α) → Decidable (Order.succ a = a)]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
WithTop.succ_coe_of_isMax
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
[(a : α) → Decidable (Order.succ a = a)]
{a : α}
(h : IsMax a)
:
theorem
WithTop.succ_coe_of_not_isMax
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
[(a : α) → Decidable (Order.succ a = a)]
{a : α}
(h : ¬IsMax a)
:
@[simp]
theorem
WithTop.succ_coe
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
[(a : α) → Decidable (Order.succ a = a)]
[NoMaxOrder α]
{a : α}
:
Equations
- WithTop.instPredOrder = { pred := fun (a : WithTop α) => match a with | none => ↑⊤ | some a => ↑(Order.pred a), pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
instance
WithTop.instIsEmptyPredOrderOfNonempty
{α : Type u_1}
[Preorder α]
[NoMaxOrder α]
[hα : Nonempty α]
:
Equations
- WithBot.instSuccOrder = { succ := fun (a : WithBot α) => match a with | none => ↑⊥ | some a => ↑(Order.succ a), le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
instance
WithBot.instPredOrder
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
[(a : α) → Decidable (Order.pred a = a)]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
WithBot.pred_coe_of_isMin
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
[(a : α) → Decidable (Order.pred a = a)]
{a : α}
(h : IsMin a)
:
theorem
WithBot.pred_coe_of_not_isMin
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
[(a : α) → Decidable (Order.pred a = a)]
{a : α}
(h : ¬IsMin a)
:
theorem
WithBot.pred_coe
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
[(a : α) → Decidable (Order.pred a = a)]
[NoMinOrder α]
{a : α}
:
Adding a ⊥ to a NoMinOrder #
instance
WithBot.instIsEmptySuccOrderOfNonempty
{α : Type u_1}
[Preorder α]
[NoMinOrder α]
[hα : Nonempty α]
:
@[reducible, inline]
abbrev
SuccOrder.ofOrderIso
{X : Type u_3}
{Y : Type u_4}
[Preorder X]
[Preorder Y]
[SuccOrder X]
(f : X ≃o Y)
:
SuccOrder transfers across equivalences between orders.
Equations
- SuccOrder.ofOrderIso f = { succ := fun (y : Y) => f (SuccOrder.succ (f.symm y)), le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
@[reducible, inline]
abbrev
PredOrder.ofOrderIso
{X : Type u_3}
{Y : Type u_4}
[Preorder X]
[Preorder Y]
[PredOrder X]
(f : X ≃o Y)
:
PredOrder transfers across equivalences between orders.
Equations
- PredOrder.ofOrderIso f = { pred := fun (y : Y) => f (PredOrder.pred (f.symm y)), pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
noncomputable instance
Set.OrdConnected.predOrder
{α : Type u_3}
[PartialOrder α]
{s : Set α}
[s.OrdConnected]
[PredOrder α]
:
PredOrder ↑s
Equations
- Set.OrdConnected.predOrder = { pred := fun (x : ↑s) => if h : Order.pred ↑x ∈ s then ⟨Order.pred ↑x, h⟩ else x, pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
@[simp]
theorem
coe_pred_of_mem
{α : Type u_3}
[PartialOrder α]
{s : Set α}
[s.OrdConnected]
[PredOrder α]
{a : ↑s}
(h : Order.pred ↑a ∈ s)
:
theorem
isMin_of_not_pred_mem
{α : Type u_3}
[PartialOrder α]
{s : Set α}
[s.OrdConnected]
[PredOrder α]
{a : ↑s}
(h : Order.pred ↑a ∉ s)
:
IsMin a
theorem
not_pred_mem_iff_isMin
{α : Type u_3}
[PartialOrder α]
{s : Set α}
[s.OrdConnected]
[PredOrder α]
[NoMinOrder α]
{a : ↑s}
:
noncomputable instance
Set.OrdConnected.succOrder
{α : Type u_3}
[PartialOrder α]
{s : Set α}
[s.OrdConnected]
[SuccOrder α]
:
SuccOrder ↑s
Equations
@[simp]
theorem
coe_succ_of_mem
{α : Type u_3}
[PartialOrder α]
{s : Set α}
[s.OrdConnected]
[SuccOrder α]
{a : ↑s}
(h : Order.succ ↑a ∈ s)
:
theorem
isMax_of_not_succ_mem
{α : Type u_3}
[PartialOrder α]
{s : Set α}
[s.OrdConnected]
[SuccOrder α]
{a : ↑s}
(h : Order.succ ↑a ∉ s)
:
IsMax a
theorem
not_succ_mem_iff_isMax
{α : Type u_3}
[PartialOrder α]
{s : Set α}
[s.OrdConnected]
[SuccOrder α]
[NoMaxOrder α]
{a : ↑s}
: