# 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.
• IsSuccArchimedean: SuccOrder where succ iterated to an element gives all the greater ones.
• IsPredArchimedean: PredOrder where pred iterated to an element gives all the smaller ones.

## Implementation notes #

Maximal elements don't have a sensible successor. Thus the naïve typeclass

class NaiveSuccOrder (α : Type*) [Preorder α] :=
(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 α.

## TODO #

Is GaloisConnection pred succ always true? If not, we should introduce

class SuccPredOrder (α : Type*) [Preorder α] extends SuccOrder α, PredOrder α :=
(pred_succ_gc : GaloisConnection (pred : α → α) succ)


CovBy should help here.

theorem SuccOrder.ext_iff {α : Type u_3} :
∀ {inst : } (x y : ), x = y SuccOrder.succ = SuccOrder.succ
theorem SuccOrder.ext {α : Type u_3} :
∀ {inst : } (x y : ), SuccOrder.succ = SuccOrder.succx = y
class SuccOrder (α : Type u_3) [] :
Type u_3

Order equipped with a sensible successor function.

• succ : αα

Successor function

• le_succ : ∀ (a : α),

Proof of basic ordering with respect to succ

• max_of_succ_le : ∀ {a : α},

Proof of interaction between succ and maximal element

• succ_le_of_lt : ∀ {a b : α}, a < b

Proof that succ satisfies ordering invariants between LT and LE

• le_of_lt_succ : ∀ {a b : α}, a b

Proof that succ satisfies ordering invariants between LE and LT

Instances
theorem SuccOrder.le_succ {α : Type u_3} [] [self : ] (a : α) :

Proof of basic ordering with respect to succ

theorem SuccOrder.max_of_succ_le {α : Type u_3} [] [self : ] {a : α} :

Proof of interaction between succ and maximal element

theorem SuccOrder.succ_le_of_lt {α : Type u_3} [] [self : ] {a : α} {b : α} :
a < b

Proof that succ satisfies ordering invariants between LT and LE

theorem SuccOrder.le_of_lt_succ {α : Type u_3} [] [self : ] {a : α} {b : α} :
a b

Proof that succ satisfies ordering invariants between LE and LT

theorem PredOrder.ext_iff {α : Type u_3} :
∀ {inst : } (x y : ), x = y PredOrder.pred = PredOrder.pred
theorem PredOrder.ext {α : Type u_3} :
∀ {inst : } (x y : ), PredOrder.pred = PredOrder.predx = y
class PredOrder (α : Type u_3) [] :
Type u_3

Order equipped with a sensible predecessor function.

• pred : αα

Predecessor function

• pred_le : ∀ (a : α),

Proof of basic ordering with respect to pred

• min_of_le_pred : ∀ {a : α},

Proof of interaction between pred and minimal element

• le_pred_of_lt : ∀ {a b : α}, a < b

Proof that pred satisfies ordering invariants between LT and LE

• le_of_pred_lt : ∀ {a b : α}, a b

Proof that pred satisfies ordering invariants between LE and LT

Instances
theorem PredOrder.pred_le {α : Type u_3} [] [self : ] (a : α) :

Proof of basic ordering with respect to pred

theorem PredOrder.min_of_le_pred {α : Type u_3} [] [self : ] {a : α} :

Proof of interaction between pred and minimal element

theorem PredOrder.le_pred_of_lt {α : Type u_3} [] [self : ] {a : α} {b : α} :
a < b

Proof that pred satisfies ordering invariants between LT and LE

theorem PredOrder.le_of_pred_lt {α : Type u_3} [] [self : ] {a : α} {b : α} :
a b

Proof that pred satisfies ordering invariants between LE and LT

instance instPredOrderOrderDualOfSuccOrder {α : Type u_1} [] [] :
Equations
• instPredOrderOrderDualOfSuccOrder = { pred := OrderDual.toDual SuccOrder.succ OrderDual.ofDual, pred_le := , min_of_le_pred := , le_pred_of_lt := , le_of_pred_lt := }
instance instSuccOrderOrderDualOfPredOrder {α : Type u_1} [] [] :
Equations
• instSuccOrderOrderDualOfPredOrder = { succ := OrderDual.toDual PredOrder.pred OrderDual.ofDual, le_succ := , max_of_succ_le := , succ_le_of_lt := , le_of_lt_succ := }
def SuccOrder.ofSuccLeIffOfLeLtSucc {α : Type u_1} [] (succ : αα) (hsucc_le_iff : ∀ {a b : α}, succ a b a < b) (hle_of_lt_succ : ∀ {a b : α}, a < succ ba b) :

A constructor for SuccOrder α usable when α has no maximal element.

Equations
• SuccOrder.ofSuccLeIffOfLeLtSucc succ hsucc_le_iff hle_of_lt_succ = { succ := succ, le_succ := , max_of_succ_le := , succ_le_of_lt := , le_of_lt_succ := }
Instances For
def PredOrder.ofLePredIffOfPredLePred {α : Type u_1} [] (pred : αα) (hle_pred_iff : ∀ {a b : α}, a pred b a < b) (hle_of_pred_lt : ∀ {a b : α}, pred a < ba b) :

A constructor for PredOrder α usable when α has no minimal element.

Equations
Instances For
@[simp]
theorem SuccOrder.ofCore_succ {α : Type u_1} [] (succ : αα) (hn : ∀ {a : α}, ¬∀ (b : α), a < b succ a b) (hm : ∀ (a : α), succ a = a) :
∀ (a : α), = succ a
def SuccOrder.ofCore {α : Type u_1} [] (succ : αα) (hn : ∀ {a : α}, ¬∀ (b : α), a < b succ a b) (hm : ∀ (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 := , le_of_lt_succ := }
Instances For
@[simp]
theorem PredOrder.ofCore_pred {α : Type u_3} [] (pred : αα) (hn : ∀ {a : α}, ¬∀ (b : α), b pred a b < a) (hm : ∀ (a : α), pred a = a) :
∀ (a : α), = pred a
def PredOrder.ofCore {α : Type u_3} [] (pred : αα) (hn : ∀ {a : α}, ¬∀ (b : α), b pred a b < a) (hm : ∀ (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 := , le_of_pred_lt := }
Instances For
def SuccOrder.ofSuccLeIff {α : Type u_1} [] (succ : αα) (hsucc_le_iff : ∀ {a b : α}, succ a b a < b) :

A constructor for SuccOrder α usable when α is a linear order with no maximal element.

Equations
• SuccOrder.ofSuccLeIff succ hsucc_le_iff = { succ := succ, le_succ := , max_of_succ_le := , succ_le_of_lt := , le_of_lt_succ := }
Instances For
def PredOrder.ofLePredIff {α : Type u_1} [] (pred : αα) (hle_pred_iff : ∀ {a b : α}, a pred b a < b) :

A constructor for PredOrder α usable when α is a linear order with no minimal element.

Equations
• PredOrder.ofLePredIff pred hle_pred_iff = { pred := pred, pred_le := , min_of_le_pred := , le_pred_of_lt := , le_of_pred_lt := }
Instances For
noncomputable def SuccOrder.ofLinearWellFoundedLT (α : Type u_1) [] [] :

A well-order is a SuccOrder.

Equations
• = SuccOrder.ofCore (fun (a : α) => if h : ().Nonempty then .min () h else a)
Instances For
noncomputable def PredOrder.ofLinearWellFoundedGT (α : Type u_3) [] [] :

A linear order with well-founded greater-than relation is a PredOrder.

Equations
Instances For

### Successor order #

def Order.succ {α : Type u_1} [] [] :
αα

The successor of an element. If a is not maximal, then succ a is the least element greater than a. If a is maximal, then succ a = a.

Equations
• Order.succ = SuccOrder.succ
Instances For
theorem Order.le_succ {α : Type u_1} [] [] (a : α) :
a
theorem Order.max_of_succ_le {α : Type u_1} [] [] {a : α} :
a
theorem Order.succ_le_of_lt {α : Type u_1} [] [] {a : α} {b : α} :
a < b b
theorem Order.le_of_lt_succ {α : Type u_1} [] [] {a : α} {b : α} :
a < a b
@[simp]
theorem Order.succ_le_iff_isMax {α : Type u_1} [] [] {a : α} :
a
@[simp]
theorem Order.lt_succ_iff_not_isMax {α : Type u_1} [] [] {a : α} :
a < ¬
theorem Order.lt_succ_of_not_isMax {α : Type u_1} [] [] {a : α} :
¬a <

Alias of the reverse direction of Order.lt_succ_iff_not_isMax.

theorem Order.wcovBy_succ {α : Type u_1} [] [] (a : α) :
a ⩿
theorem Order.covBy_succ_of_not_isMax {α : Type u_1} [] [] {a : α} (h : ¬) :
a
theorem Order.lt_succ_iff_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) :
b < b a
theorem Order.succ_le_iff_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) :
b a < b
theorem Order.succ_lt_succ_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (h : a < b) (hb : ¬) :
theorem Order.succ_lt_succ_iff_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) (hb : ¬) :
a < b
theorem Order.succ_le_succ_iff_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) (hb : ¬) :
a b
@[simp]
theorem Order.succ_le_succ {α : Type u_1} [] [] {a : α} {b : α} (h : a b) :
theorem Order.succ_mono {α : Type u_1} [] [] :
Monotone Order.succ
theorem Order.le_succ_iterate {α : Type u_1} [] [] (k : ) (x : α) :
x Order.succ^[k] x
theorem Order.isMax_iterate_succ_of_eq_of_lt {α : Type u_1} [] [] {a : α} {n : } {m : } (h_eq : Order.succ^[n] a = Order.succ^[m] a) (h_lt : n < m) :
IsMax (Order.succ^[n] a)
theorem Order.isMax_iterate_succ_of_eq_of_ne {α : Type u_1} [] [] {a : α} {n : } {m : } (h_eq : Order.succ^[n] a = Order.succ^[m] a) (h_ne : n m) :
IsMax (Order.succ^[n] a)
theorem Order.Iio_succ_of_not_isMax {α : Type u_1} [] [] {a : α} (ha : ¬) :
=
theorem Order.Ici_succ_of_not_isMax {α : Type u_1} [] [] {a : α} (ha : ¬) :
=
theorem Order.Ico_succ_right_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (hb : ¬) :
Set.Ico a () = Set.Icc a b
theorem Order.Ioo_succ_right_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (hb : ¬) :
Set.Ioo a () = Set.Ioc a b
theorem Order.Icc_succ_left_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) :
Set.Icc () b = Set.Ioc a b
theorem Order.Ico_succ_left_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) :
Set.Ico () b = Set.Ioo a b
theorem Order.lt_succ {α : Type u_1} [] [] [] (a : α) :
a <
@[simp]
theorem Order.lt_succ_iff {α : Type u_1} [] [] {a : α} {b : α} [] :
a < a b
@[simp]
theorem Order.succ_le_iff {α : Type u_1} [] [] {a : α} {b : α} [] :
b a < b
theorem Order.succ_le_succ_iff {α : Type u_1} [] [] {a : α} {b : α} [] :
a b
theorem Order.succ_lt_succ_iff {α : Type u_1} [] [] {a : α} {b : α} [] :
a < b
theorem Order.le_of_succ_le_succ {α : Type u_1} [] [] {a : α} {b : α} [] :
a b

Alias of the forward direction of Order.succ_le_succ_iff.

theorem Order.succ_lt_succ {α : Type u_1} [] [] {a : α} {b : α} [] :
a < b

Alias of the reverse direction of Order.succ_lt_succ_iff.

theorem Order.lt_of_succ_lt_succ {α : Type u_1} [] [] {a : α} {b : α} [] :
a < b

Alias of the forward direction of Order.succ_lt_succ_iff.

theorem Order.succ_strictMono {α : Type u_1} [] [] [] :
StrictMono Order.succ
theorem Order.covBy_succ {α : Type u_1} [] [] [] (a : α) :
a
@[simp]
theorem Order.Iio_succ {α : Type u_1} [] [] [] (a : α) :
=
@[simp]
theorem Order.Ici_succ {α : Type u_1} [] [] [] (a : α) :
=
@[simp]
theorem Order.Ico_succ_right {α : Type u_1} [] [] [] (a : α) (b : α) :
Set.Ico a () = Set.Icc a b
@[simp]
theorem Order.Ioo_succ_right {α : Type u_1} [] [] [] (a : α) (b : α) :
Set.Ioo a () = Set.Ioc a b
@[simp]
theorem Order.Icc_succ_left {α : Type u_1} [] [] [] (a : α) (b : α) :
Set.Icc () b = Set.Ioc a b
@[simp]
theorem Order.Ico_succ_left {α : Type u_1} [] [] [] (a : α) (b : α) :
Set.Ico () b = Set.Ioo a b
@[simp]
theorem Order.succ_eq_iff_isMax {α : Type u_1} [] [] {a : α} :
= a
theorem IsMax.succ_eq {α : Type u_1} [] [] {a : α} :
= a

Alias of the reverse direction of Order.succ_eq_iff_isMax.

theorem Order.succ_eq_succ_iff_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) (hb : ¬) :
a = b
theorem Order.le_le_succ_iff {α : Type u_1} [] [] {a : α} {b : α} :
a b b b = a b =
theorem CovBy.succ_eq {α : Type u_1} [] [] {a : α} {b : α} (h : a b) :
= b
theorem WCovBy.le_succ {α : Type u_1} [] [] {a : α} {b : α} (h : a ⩿ b) :
b
theorem Order.le_succ_iff_eq_or_le {α : Type u_1} [] [] {a : α} {b : α} :
a a = a b
theorem Order.lt_succ_iff_eq_or_lt_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (hb : ¬) :
a < a = b a < b
theorem Order.Iic_succ {α : Type u_1} [] [] (a : α) :
= insert () ()
theorem Order.Icc_succ_right {α : Type u_1} [] [] {a : α} {b : α} (h : a ) :
Set.Icc a () = insert () (Set.Icc a b)
theorem Order.Ioc_succ_right {α : Type u_1} [] [] {a : α} {b : α} (h : a < ) :
Set.Ioc a () = insert () (Set.Ioc a b)
theorem Order.Iio_succ_eq_insert_of_not_isMax {α : Type u_1} [] [] {a : α} (h : ¬) :
= insert a ()
theorem Order.Ico_succ_right_eq_insert_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (h₁ : a b) (h₂ : ¬) :
Set.Ico a () = insert b (Set.Ico a b)
theorem Order.Ioo_succ_right_eq_insert_of_not_isMax {α : Type u_1} [] [] {a : α} {b : α} (h₁ : a < b) (h₂ : ¬) :
Set.Ioo a () = insert b (Set.Ioo a b)
@[simp]
theorem Order.succ_eq_succ_iff {α : Type u_1} [] [] {a : α} {b : α} [] :
a = b
theorem Order.succ_injective {α : Type u_1} [] [] [] :
theorem Order.succ_ne_succ_iff {α : Type u_1} [] [] {a : α} {b : α} [] :
a b
theorem Order.succ_ne_succ {α : Type u_1} [] [] {a : α} {b : α} [] :
a b

Alias of the reverse direction of Order.succ_ne_succ_iff.

theorem Order.lt_succ_iff_eq_or_lt {α : Type u_1} [] [] {a : α} {b : α} [] :
a < a = b a < b
theorem Order.succ_eq_iff_covBy {α : Type u_1} [] [] {a : α} {b : α} [] :
= b a b
theorem Order.Iio_succ_eq_insert {α : Type u_1} [] [] [] (a : α) :
= insert a ()
theorem Order.Ico_succ_right_eq_insert {α : Type u_1} [] [] {a : α} {b : α} [] (h : a b) :
Set.Ico a () = insert b (Set.Ico a b)
theorem Order.Ioo_succ_right_eq_insert {α : Type u_1} [] [] {a : α} {b : α} [] (h : a < b) :
Set.Ioo a () = insert b (Set.Ioo a b)
@[simp]
theorem Order.succ_top {α : Type u_1} [] [] [] :
theorem Order.succ_le_iff_eq_top {α : Type u_1} [] [] {a : α} [] :
a a =
theorem Order.lt_succ_iff_ne_top {α : Type u_1} [] [] {a : α} [] :
a < a
theorem Order.lt_succ_bot_iff {α : Type u_1} [] [] {a : α} [] [] :
a =
theorem Order.le_succ_bot_iff {α : Type u_1} [] [] {a : α} [] :
a =
theorem Order.bot_lt_succ {α : Type u_1} [] [] [] [] (a : α) :
theorem Order.succ_ne_bot {α : Type u_1} [] [] [] [] (a : α) :
instance Order.instSubsingletonSuccOrder {α : Type u_1} [] :

There is at most one way to define the successors in a PartialOrder.

Equations
• =
theorem Order.succ_eq_iInf {α : Type u_1} [] [] (a : α) :
= ⨅ (b : α), ⨅ (_ : a < b), b

### Predecessor order #

def Order.pred {α : Type u_1} [] [] :
αα

The predecessor of an element. If a is not minimal, then pred a is the greatest element less than a. If a is minimal, then pred a = a.

Equations
• Order.pred = PredOrder.pred
Instances For
theorem Order.pred_le {α : Type u_1} [] [] (a : α) :
a
theorem Order.min_of_le_pred {α : Type u_1} [] [] {a : α} :
a
theorem Order.le_pred_of_lt {α : Type u_1} [] [] {a : α} {b : α} :
a < ba
theorem Order.le_of_pred_lt {α : Type u_1} [] [] {a : α} {b : α} :
< ba b
@[simp]
theorem Order.le_pred_iff_isMin {α : Type u_1} [] [] {a : α} :
a
@[simp]
theorem Order.pred_lt_iff_not_isMin {α : Type u_1} [] [] {a : α} :
< a ¬
theorem Order.pred_lt_of_not_isMin {α : Type u_1} [] [] {a : α} :
¬ < a

Alias of the reverse direction of Order.pred_lt_iff_not_isMin.

theorem Order.pred_wcovBy {α : Type u_1} [] [] (a : α) :
⩿ a
theorem Order.pred_covBy_of_not_isMin {α : Type u_1} [] [] {a : α} (h : ¬) :
a
theorem Order.pred_lt_iff_of_not_isMin {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) :
< b a b
theorem Order.le_pred_iff_of_not_isMin {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) :
b b < a
theorem Order.pred_lt_pred_of_not_isMin {α : Type u_1} [] [] {a : α} {b : α} (h : a < b) (ha : ¬) :
theorem Order.pred_lt_pred_iff_of_not_isMin {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) (hb : ¬) :
a < b
theorem Order.pred_le_pred_iff_of_not_isMin {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) (hb : ¬) :
a b
@[simp]
theorem Order.pred_le_pred {α : Type u_1} [] [] {a : α} {b : α} (h : a b) :
theorem Order.pred_mono {α : Type u_1} [] [] :
Monotone Order.pred
theorem Order.pred_iterate_le {α : Type u_1} [] [] (k : ) (x : α) :
Order.pred^[k] x x
theorem Order.isMin_iterate_pred_of_eq_of_lt {α : Type u_1} [] [] {a : α} {n : } {m : } (h_eq : Order.pred^[n] a = Order.pred^[m] a) (h_lt : n < m) :
IsMin (Order.pred^[n] a)
theorem Order.isMin_iterate_pred_of_eq_of_ne {α : Type u_1} [] [] {a : α} {n : } {m : } (h_eq : Order.pred^[n] a = Order.pred^[m] a) (h_ne : n m) :
IsMin (Order.pred^[n] a)
theorem Order.Ioi_pred_of_not_isMin {α : Type u_1} [] [] {a : α} (ha : ¬) :
=
theorem Order.Iic_pred_of_not_isMin {α : Type u_1} [] [] {a : α} (ha : ¬) :
=
theorem Order.Ioc_pred_left_of_not_isMin {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) :
Set.Ioc () b = Set.Icc a b
theorem Order.Ioo_pred_left_of_not_isMin {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) :
Set.Ioo () b = Set.Ico a b
theorem Order.Icc_pred_right_of_not_isMin {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) :
Set.Icc a () = Set.Ico a b
theorem Order.Ioc_pred_right_of_not_isMin {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) :
Set.Ioc a () = Set.Ioo a b
theorem Order.pred_lt {α : Type u_1} [] [] [] (a : α) :
< a
@[simp]
theorem Order.pred_lt_iff {α : Type u_1} [] [] {a : α} {b : α} [] :
< b a b
@[simp]
theorem Order.le_pred_iff {α : Type u_1} [] [] {a : α} {b : α} [] :
a a < b
theorem Order.pred_le_pred_iff {α : Type u_1} [] [] {a : α} {b : α} [] :
a b
theorem Order.pred_lt_pred_iff {α : Type u_1} [] [] {a : α} {b : α} [] :
a < b
theorem Order.le_of_pred_le_pred {α : Type u_1} [] [] {a : α} {b : α} [] :
a b

Alias of the forward direction of Order.pred_le_pred_iff.

theorem Order.pred_lt_pred {α : Type u_1} [] [] {a : α} {b : α} [] :
a < b

Alias of the reverse direction of Order.pred_lt_pred_iff.

theorem Order.lt_of_pred_lt_pred {α : Type u_1} [] [] {a : α} {b : α} [] :
a < b

Alias of the forward direction of Order.pred_lt_pred_iff.

theorem Order.pred_strictMono {α : Type u_1} [] [] [] :
StrictMono Order.pred
theorem Order.pred_covBy {α : Type u_1} [] [] [] (a : α) :
a
@[simp]
theorem Order.Ioi_pred {α : Type u_1} [] [] [] (a : α) :
=
@[simp]
theorem Order.Iic_pred {α : Type u_1} [] [] [] (a : α) :
=
@[simp]
theorem Order.Ioc_pred_left {α : Type u_1} [] [] [] (a : α) (b : α) :
Set.Ioc () b = Set.Icc a b
@[simp]
theorem Order.Ioo_pred_left {α : Type u_1} [] [] [] (a : α) (b : α) :
Set.Ioo () b = Set.Ico a b
@[simp]
theorem Order.Icc_pred_right {α : Type u_1} [] [] [] (a : α) (b : α) :
Set.Icc a () = Set.Ico a b
@[simp]
theorem Order.Ioc_pred_right {α : Type u_1} [] [] [] (a : α) (b : α) :
Set.Ioc a () = Set.Ioo a b
@[simp]
theorem Order.pred_eq_iff_isMin {α : Type u_1} [] [] {a : α} :
= a
theorem IsMin.pred_eq {α : Type u_1} [] [] {a : α} :
= a

Alias of the reverse direction of Order.pred_eq_iff_isMin.

theorem Order.pred_eq_pred_iff_of_not_isMin {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) (hb : ¬) :
a = b
theorem Order.pred_le_le_iff {α : Type u_1} [] [] {a : α} {b : α} :
b b a b = a b =
theorem CovBy.pred_eq {α : Type u_1} [] [] {a : α} {b : α} (h : a b) :
= a
theorem WCovBy.pred_le {α : Type u_1} [] [] {a : α} {b : α} (h : a ⩿ b) :
a
theorem Order.pred_le_iff_eq_or_le {α : Type u_1} [] [] {a : α} {b : α} :
b b = a b
theorem Order.pred_lt_iff_eq_or_lt_of_not_isMin {α : Type u_1} [] [] {a : α} {b : α} (ha : ¬) :
< b a = b a < b
theorem Order.Ici_pred {α : Type u_1} [] [] (a : α) :
= insert () ()
theorem Order.Ioi_pred_eq_insert_of_not_isMin {α : Type u_1} [] [] {a : α} (ha : ¬) :
= insert a ()
theorem Order.Icc_pred_left {α : Type u_1} [] [] {a : α} {b : α} (h : b) :
Set.Icc () b = insert () (Set.Icc a b)
theorem Order.Ico_pred_left {α : Type u_1} [] [] {a : α} {b : α} (h : < b) :
Set.Ico () b = insert () (Set.Ico a b)
@[simp]
theorem Order.pred_eq_pred_iff {α : Type u_1} [] [] {a : α} {b : α} [] :
a = b
theorem Order.pred_injective {α : Type u_1} [] [] [] :
theorem Order.pred_ne_pred_iff {α : Type u_1} [] [] {a : α} {b : α} [] :
a b
theorem Order.pred_ne_pred {α : Type u_1} [] [] {a : α} {b : α} [] :
a b

Alias of the reverse direction of Order.pred_ne_pred_iff.

theorem Order.pred_lt_iff_eq_or_lt {α : Type u_1} [] [] {a : α} {b : α} [] :
< b a = b a < b
theorem Order.pred_eq_iff_covBy {α : Type u_1} [] [] {a : α} {b : α} [] :
= a a b
theorem Order.Ioi_pred_eq_insert {α : Type u_1} [] [] [] (a : α) :
= insert a ()
theorem Order.Ico_pred_right_eq_insert {α : Type u_1} [] [] {a : α} {b : α} [] (h : a b) :
Set.Ioc () b = insert a (Set.Ioc a b)
theorem Order.Ioo_pred_right_eq_insert {α : Type u_1} [] [] {a : α} {b : α} [] (h : a < b) :
Set.Ioo () b = insert a (Set.Ioo a b)
@[simp]
theorem Order.pred_bot {α : Type u_1} [] [] [] :
theorem Order.le_pred_iff_eq_bot {α : Type u_1} [] [] {a : α} [] :
a a =
theorem Order.pred_lt_iff_ne_bot {α : Type u_1} [] [] {a : α} [] :
< a a
theorem Order.pred_top_lt_iff {α : Type u_1} [] [] {a : α} [] [] :
a =
theorem Order.pred_top_le_iff {α : Type u_1} [] [] {a : α} [] :
a =
theorem Order.pred_lt_top {α : Type u_1} [] [] [] [] (a : α) :
theorem Order.pred_ne_top {α : Type u_1} [] [] [] [] (a : α) :
instance Order.instSubsingletonPredOrder {α : Type u_1} [] :

There is at most one way to define the predecessors in a PartialOrder.

Equations
• =
theorem Order.pred_eq_iSup {α : Type u_1} [] [] (a : α) :
= ⨆ (b : α), ⨆ (_ : b < a), b

### Successor-predecessor orders #

@[simp]
theorem Order.succ_pred_of_not_isMin {α : Type u_1} [] [] [] {a : α} (h : ¬) :
= a
@[simp]
theorem Order.pred_succ_of_not_isMax {α : Type u_1} [] [] [] {a : α} (h : ¬) :
= a
theorem Order.succ_pred {α : Type u_1} [] [] [] [] (a : α) :
= a
theorem Order.pred_succ {α : Type u_1} [] [] [] [] (a : α) :
= a
theorem Order.pred_succ_iterate_of_not_isMax {α : Type u_1} [] [] [] (i : α) (n : ) (hin : ¬IsMax (Order.succ^[n - 1] i)) :
Order.pred^[n] (Order.succ^[n] i) = i
theorem Order.succ_pred_iterate_of_not_isMin {α : Type u_1} [] [] [] (i : α) (n : ) (hin : ¬IsMin (Order.pred^[n - 1] i)) :
Order.succ^[n] (Order.pred^[n] i) = i

### 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 an OrderTop: Preserves succ and pred.
• Adding a ⊤ to a NoMaxOrder: Preserves succ. Never preserves pred.
• Adding a ⊥ to an OrderBot: Preserves succ and pred.
• Adding a ⊥ to a NoMinOrder: Preserves pred. Never preserves succ. where "preserves (succ/pred)" means (Succ/Pred)Order α → (Succ/Pred)Order ((WithTop/WithBot) α).

#### Adding a ⊤ to an OrderTop#

instance WithTop.instSuccOrder {α : Type u_1} [] [] [] [] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem WithTop.succ_coe_top {α : Type u_1} [] [] [] [] :
theorem WithTop.succ_coe_of_ne_top {α : Type u_1} [] [] [] [] {a : α} (h : a ) :
= ()
instance WithTop.instPredOrder {α : Type u_1} [] [] [] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem WithTop.pred_top {α : Type u_1} [] [] [] :
@[simp]
theorem WithTop.pred_coe {α : Type u_1} [] [] [] (a : α) :
= ()
@[simp]
theorem WithTop.pred_untop {α : Type u_1} [] [] [] (a : ) (ha : a ) :
Order.pred (a.untop ha) = ().untop

#### Adding a ⊤ to a NoMaxOrder#

instance WithTop.succOrderOfNoMaxOrder {α : Type u_1} [] [] [] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem WithTop.succ_coe {α : Type u_1} [] [] [] (a : α) :
= ()
instance WithTop.instIsEmptyPredOrderOfNonempty {α : Type u_1} [] [] [hα : ] :
Equations
• =

#### Adding a ⊥ to an OrderBot#

instance WithBot.instSuccOrder {α : Type u_1} [] [] [] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem WithBot.succ_bot {α : Type u_1} [] [] [] :
@[simp]
theorem WithBot.succ_coe {α : Type u_1} [] [] [] (a : α) :
= ()
@[simp]
theorem WithBot.succ_unbot {α : Type u_1} [] [] [] (a : ) (ha : a ) :
Order.succ (a.unbot ha) = ().unbot
instance WithBot.instPredOrder {α : Type u_1} [] [] [] [] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem WithBot.pred_coe_bot {α : Type u_1} [] [] [] [] :
theorem WithBot.pred_coe_of_ne_bot {α : Type u_1} [] [] [] [] {a : α} (h : a ) :
= ()

#### Adding a ⊥ to a NoMinOrder#

instance WithBot.instIsEmptySuccOrderOfNonempty {α : Type u_1} [] [] [hα : ] :
Equations
• =
instance WithBot.predOrderOfNoMinOrder {α : Type u_1} [] [] [] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem WithBot.pred_coe {α : Type u_1} [] [] [] (a : α) :
= ()

### Archimedeanness #

class IsSuccArchimedean (α : Type u_3) [] [] :

A SuccOrder is succ-archimedean if one can go from any two comparable elements by iterating succ

• exists_succ_iterate_of_le : ∀ {a b : α}, a b∃ (n : ), Order.succ^[n] a = b

If a ≤ b then one can get to a from b by iterating succ

Instances
theorem IsSuccArchimedean.exists_succ_iterate_of_le {α : Type u_3} [] [] [self : ] {a : α} {b : α} (h : a b) :
∃ (n : ), Order.succ^[n] a = b

If a ≤ b then one can get to a from b by iterating succ

class IsPredArchimedean (α : Type u_3) [] [] :

A PredOrder is pred-archimedean if one can go from any two comparable elements by iterating pred

• exists_pred_iterate_of_le : ∀ {a b : α}, a b∃ (n : ), Order.pred^[n] b = a

If a ≤ b then one can get to b from a by iterating pred

Instances
theorem IsPredArchimedean.exists_pred_iterate_of_le {α : Type u_3} [] [] [self : ] {a : α} {b : α} (h : a b) :
∃ (n : ), Order.pred^[n] b = a

If a ≤ b then one can get to b from a by iterating pred

instance instIsPredArchimedeanOrderDual {α : Type u_1} [] [] :
Equations
• =
theorem LE.le.exists_succ_iterate {α : Type u_1} [] [] {a : α} {b : α} (h : a b) :
∃ (n : ), Order.succ^[n] a = b
theorem exists_succ_iterate_iff_le {α : Type u_1} [] [] {a : α} {b : α} :
(∃ (n : ), Order.succ^[n] a = b) a b
theorem Succ.rec {α : Type u_1} [] [] {P : αProp} {m : α} (h0 : P m) (h1 : ∀ (n : α), m nP nP ()) ⦃n : α (hmn : m n) :
P n

Induction principle on a type with a SuccOrder for all elements above a given element m.

theorem Succ.rec_iff {α : Type u_1} [] [] {p : αProp} (hsucc : ∀ (a : α), p a p ()) {a : α} {b : α} (h : a b) :
p a p b
instance instIsSuccArchimedeanOrderDual {α : Type u_1} [] [] :
Equations
• =
theorem LE.le.exists_pred_iterate {α : Type u_1} [] [] {a : α} {b : α} (h : a b) :
∃ (n : ), Order.pred^[n] b = a
theorem exists_pred_iterate_iff_le {α : Type u_1} [] [] {a : α} {b : α} :
(∃ (n : ), Order.pred^[n] b = a) a b
theorem Pred.rec {α : Type u_1} [] [] {P : αProp} {m : α} (h0 : P m) (h1 : nm, P nP ()) ⦃n : α (hmn : n m) :
P n

Induction principle on a type with a PredOrder for all elements below a given element m.

theorem Pred.rec_iff {α : Type u_1} [] [] {p : αProp} (hsucc : ∀ (a : α), p a p ()) {a : α} {b : α} (h : a b) :
p a p b
theorem succ_max {α : Type u_1} [] [] (a : α) (b : α) :
Order.succ (max a b) = max () ()
theorem succ_min {α : Type u_1} [] [] (a : α) (b : α) :
Order.succ (min a b) = min () ()
theorem exists_succ_iterate_or {α : Type u_1} [] [] {a : α} {b : α} :
(∃ (n : ), Order.succ^[n] a = b) ∃ (n : ), Order.succ^[n] b = a
theorem Succ.rec_linear {α : Type u_1} [] [] {p : αProp} (hsucc : ∀ (a : α), p a p ()) (a : α) (b : α) :
p a p b
theorem pred_max {α : Type u_1} [] [] (a : α) (b : α) :
Order.pred (max a b) = max () ()
theorem pred_min {α : Type u_1} [] [] (a : α) (b : α) :
Order.pred (min a b) = min () ()
theorem exists_pred_iterate_or {α : Type u_1} [] [] {a : α} {b : α} :
(∃ (n : ), Order.pred^[n] b = a) ∃ (n : ), Order.pred^[n] a = b
theorem Pred.rec_linear {α : Type u_1} [] [] {p : αProp} (hsucc : ∀ (a : α), p a p ()) (a : α) (b : α) :
p a p b
theorem StrictMono.not_bddAbove_range {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} [] [] (hf : ) :
theorem StrictMono.not_bddBelow_range {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} [] [] (hf : ) :
theorem StrictAnti.not_bddAbove_range {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} [] [] (hf : ) :
theorem StrictAnti.not_bddBelow_range {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} [] [] (hf : ) :
@[instance 100]
instance IsWellOrder.toIsPredArchimedean {α : Type u_1} [] [h : IsWellOrder α fun (x x_1 : α) => x < x_1] [] :
Equations
• =
@[instance 100]
instance IsWellOrder.toIsSuccArchimedean {α : Type u_1} [] [h : IsWellOrder α fun (x x_1 : α) => x > x_1] [] :
Equations
• =
theorem Succ.rec_bot {α : Type u_1} [] [] [] (p : αProp) (hbot : p ) (hsucc : ∀ (a : α), p ap ()) (a : α) :
p a
theorem Pred.rec_top {α : Type u_1} [] [] [] (p : αProp) (htop : p ) (hpred : ∀ (a : α), p ap ()) (a : α) :
p a
theorem SuccOrder.forall_ne_bot_iff {α : Type u_1} [] [] [] [] (P : αProp) :
(∀ (i : α), i P i) ∀ (i : α), P ()