order.succ_pred

# 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...

## Implementation notes #

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

class naive_succ_order (α : 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 order_top 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 maximal_of_succ_le). The stricter condition of every element having a sensible successor can be obtained through the combination of succ_order α and no_top_order α.

## TODO #

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

class succ_pred_order (α : Type*) [preorder α] extends succ_order α, pred_order α :=
(pred_succ_gc : galois_connection (pred : α  α) succ)

This gives succ (pred n) = n and pred (succ n) for free when no_bot_order α and no_top_order α respectively.

### Successor order #

@[ext, class]
structure succ_order (α : Type u_2) [preorder α] :
Type u_2
• succ : α → α
• le_succ : ∀ (a : α),
• maximal_of_succ_le : ∀ ⦃a : α⦄, ∀ ⦃b : α⦄, ¬a < b
• succ_le_of_lt : ∀ {a b : α}, a < b
• le_of_lt_succ : ∀ {a b : α}, a b

Order equipped with a sensible successor function.

Instances
theorem succ_order.ext {α : Type u_2} {_inst_1 : preorder α} (x y : succ_order α)  :
x = y
theorem succ_order.ext_iff {α : Type u_2} {_inst_1 : preorder α} (x y : succ_order α) :
def succ_order.of_succ_le_iff_of_le_lt_succ {α : Type u_1} [preorder α] (succ : α → α) (hsucc_le_iff : ∀ {a b : α}, succ a b a < b) (hle_of_lt_succ : ∀ {a b : α}, a < succ ba b) :

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

Equations
@[simp]
theorem succ_order.succ_le_succ {α : Type u_1} [preorder α] [succ_order α] {a b : α} (h : a b) :
theorem succ_order.succ_mono {α : Type u_1} [preorder α] [succ_order α] :
theorem succ_order.lt_succ_of_not_maximal {α : Type u_1} [preorder α] [succ_order α] {a b : α} (h : a < b) :
theorem succ_order.lt_succ {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] (a : α) :
theorem succ_order.lt_succ_iff {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] {a b : α} :
a b
theorem succ_order.succ_le_iff {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] {a b : α} :
a < b
@[simp]
theorem succ_order.succ_le_succ_iff {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] {a b : α} :
a b
theorem le_of_succ_le_succ {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] {a b : α} :
a b

Alias of succ_le_succ_iff.

theorem succ_order.succ_lt_succ_iff {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] {a b : α} :
a < b
theorem succ_lt_succ {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] {a b : α} :
a < b

Alias of succ_lt_succ_iff.

theorem lt_of_succ_lt_succ {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] {a b : α} :
a < b

Alias of succ_lt_succ_iff.

theorem succ_order.succ_strict_mono {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] :
@[protected, instance]
def succ_order.subsingleton {α : Type u_1}  :

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

theorem succ_order.le_le_succ_iff {α : Type u_1} [succ_order α] {a b : α} :
a b b = a
theorem succ_order.succ_injective {α : Type u_1} [succ_order α] [no_top_order α] :
theorem succ_order.succ_eq_succ_iff {α : Type u_1} [succ_order α] [no_top_order α] {a b : α} :
a = b
theorem succ_order.succ_ne_succ_iff {α : Type u_1} [succ_order α] [no_top_order α] {a b : α} :
a b
theorem succ_ne_succ {α : Type u_1} [succ_order α] [no_top_order α] {a b : α} :
a b

Alias of succ_ne_succ_iff.

theorem ne_of_succ_ne_succ {α : Type u_1} [succ_order α] [no_top_order α] {a b : α} :
a b

Alias of succ_ne_succ_iff.

theorem succ_order.lt_succ_iff_lt_or_eq {α : Type u_1} [succ_order α] [no_top_order α] {a b : α} :
a < b a = b
theorem succ_order.le_succ_iff_lt_or_eq {α : Type u_1} [succ_order α] [no_top_order α] {a b : α} :
a b
@[simp]
theorem succ_order.succ_top {α : Type u_1} [order_top α] [succ_order α] :
@[simp]
theorem succ_order.succ_le_iff_eq_top {α : Type u_1} [order_top α] [succ_order α] {a : α} :
a =
@[simp]
theorem succ_order.lt_succ_iff_ne_top {α : Type u_1} [order_top α] [succ_order α] {a : α} :
theorem succ_order.bot_lt_succ {α : Type u_1} [order_bot α] [succ_order α] [nontrivial α] (a : α) :
theorem succ_order.succ_ne_bot {α : Type u_1} [order_bot α] [succ_order α] [nontrivial α] (a : α) :
def succ_order.of_succ_le_iff {α : Type u_1} [linear_order α] (succ : α → α) (hsucc_le_iff : ∀ {a b : α}, succ a b a < b) :

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

Equations
theorem succ_order.succ_eq_infi {α : Type u_1} [succ_order α] (a : α) :
= ⨅ (b : α) (h : a < b), b

### Predecessor order #

theorem pred_order.ext_iff {α : Type u_2} {_inst_1 : preorder α} (x y : pred_order α) :
@[ext, class]
structure pred_order (α : Type u_2) [preorder α] :
Type u_2
• pred : α → α
• pred_le : ∀ (a : α),
• minimal_of_le_pred : ∀ ⦃a : α⦄, ∀ ⦃b : α⦄, ¬b < a
• le_pred_of_lt : ∀ {a b : α}, a < b
• le_of_pred_lt : ∀ {a b : α}, a b

Order equipped with a sensible predecessor function.

Instances
theorem pred_order.ext {α : Type u_2} {_inst_1 : preorder α} (x y : pred_order α)  :
x = y
def pred_order.of_le_pred_iff_of_pred_le_pred {α : Type u_1} [preorder α] (pred : α → α) (hle_pred_iff : ∀ {a b : α}, a pred b a < b) (hle_of_pred_lt : ∀ {a b : α}, pred a < ba b) :

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

Equations
@[simp]
theorem pred_order.pred_le_pred {α : Type u_1} [preorder α] [pred_order α] {a b : α} (h : a b) :
theorem pred_order.pred_mono {α : Type u_1} [preorder α] [pred_order α] :
theorem pred_order.pred_lt_of_not_minimal {α : Type u_1} [preorder α] [pred_order α] {a b : α} (h : b < a) :
theorem pred_order.pred_lt {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] (a : α) :
theorem pred_order.pred_lt_iff {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] {a b : α} :
a b
theorem pred_order.le_pred_iff {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] {a b : α} :
a < b
@[simp]
theorem pred_order.pred_le_pred_iff {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] {a b : α} :
a b
theorem le_of_pred_le_pred {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] {a b : α} :
a b

Alias of pred_le_pred_iff.

@[simp]
theorem pred_order.pred_lt_pred_iff {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] {a b : α} :
a < b
theorem pred_lt_pred {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] {a b : α} :
a < b

Alias of pred_lt_pred_iff.

theorem lt_of_pred_lt_pred {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] {a b : α} :
a < b

Alias of pred_lt_pred_iff.

theorem pred_order.pred_strict_mono {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] :
@[protected, instance]
def pred_order.subsingleton {α : Type u_1}  :

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

theorem pred_order.pred_le_le_iff {α : Type u_1} [pred_order α] {a b : α} :
b a b = a
theorem pred_order.pred_injective {α : Type u_1} [pred_order α] [no_bot_order α] :
theorem pred_order.pred_eq_pred_iff {α : Type u_1} [pred_order α] [no_bot_order α] {a b : α} :
a = b
theorem pred_order.pred_ne_pred_iff {α : Type u_1} [pred_order α] [no_bot_order α] {a b : α} :
a b
theorem pred_order.pred_lt_iff_lt_or_eq {α : Type u_1} [pred_order α] [no_bot_order α] {a b : α} :
a < b a = b
theorem pred_order.le_pred_iff_lt_or_eq {α : Type u_1} [pred_order α] [no_bot_order α] {a b : α} :
a b
@[simp]
theorem pred_order.pred_bot {α : Type u_1} [order_bot α] [pred_order α] :
@[simp]
theorem pred_order.le_pred_iff_eq_bot {α : Type u_1} [order_bot α] [pred_order α] {a : α} :
a =
@[simp]
theorem pred_order.pred_lt_iff_ne_bot {α : Type u_1} [order_bot α] [pred_order α] {a : α} :
theorem pred_order.pred_lt_top {α : Type u_1} [order_top α] [pred_order α] [nontrivial α] (a : α) :
theorem pred_order.pred_ne_top {α : Type u_1} [order_top α] [pred_order α] [nontrivial α] (a : α) :
def pred_order.of_le_pred_iff {α : Type u_1} [linear_order α] (pred : α → α) (hle_pred_iff : ∀ {a b : α}, a pred b a < b) :

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

Equations
theorem pred_order.pred_eq_supr {α : Type u_1} [pred_order α] (a : α) :
= ⨆ (b : α) (h : b < a), b

### Dual order #

@[protected, instance]
def order_dual.succ_order {α : Type u_1} [preorder α] [pred_order α] :
Equations
@[protected, instance]
def order_dual.pred_order {α : Type u_1} [preorder α] [succ_order α] :
Equations

### with_bot, with_top#

Adding a greatest/least element to a succ_order or to a pred_order.

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 order_top: Preserves succ and pred.
• Adding a to a no_top_order: Preserves succ. Never preserves pred.
• Adding a to an order_bot: Preserves succ and pred.
• Adding a to a no_bot_order: Preserves pred. Never preserves succ. where "preserves (succ/pred)" means (succ/pred)_order α → (succ/pred)_order ((with_top/with_bot) α).

#### Adding a ⊤ to an order_top#

@[protected, instance]
def with_top.succ_order {α : Type u_1} [decidable_eq α] [order_top α] [succ_order α] :
Equations
@[protected, instance]
def with_top.pred_order {α : Type u_1} [order_top α] [pred_order α] :
Equations

#### Adding a ⊤ to a no_top_order#

@[protected, instance]
def of_no_top {α : Type u_1} [no_top_order α] [succ_order α] :
Equations
@[protected, instance]
def pred_order.is_empty {α : Type u_1} [no_top_order α] [hα : nonempty α] :

#### Adding a ⊥ to a bot_order#

@[protected, instance]
def with_bot.succ_order {α : Type u_1} [preorder α] [order_bot α] [succ_order α] :
Equations
@[protected, instance]
def with_bot.pred_order {α : Type u_1} [decidable_eq α] [order_bot α] [pred_order α] :
Equations

#### Adding a ⊥ to a no_bot_order#

@[protected, instance]
def succ_order.is_empty {α : Type u_1} [no_bot_order α] [hα : nonempty α] :
@[protected, instance]
def of_no_bot {α : Type u_1} [no_bot_order α] [pred_order α] :
Equations

### Archimedeanness #

@[class]
structure is_succ_archimedean (α : Type u_2) [preorder α] [succ_order α] :
Prop
• exists_succ_iterate_of_le : ∀ {a b : α}, a b(∃ (n : ), = b)

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

Instances
@[class]
structure is_pred_archimedean (α : Type u_2) [preorder α] [pred_order α] :
Prop
• exists_pred_iterate_of_le : ∀ {a b : α}, a b(∃ (n : ), = a)

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

Instances
@[protected, instance]
def order_dual.is_pred_archimedean {α : Type u_1} [preorder α] [succ_order α]  :
theorem has_le.le.exists_succ_iterate {α : Type u_1} [preorder α] [succ_order α] {a b : α} (h : a b) :
∃ (n : ),
theorem exists_succ_iterate_iff_le {α : Type u_1} [preorder α] [succ_order α] {a b : α} :
(∃ (n : ), = b) a b
theorem succ.rec {α : Type u_1} [preorder α] [succ_order α] {p : α → Prop} (hsucc : ∀ (a : α), p ap ) {a b : α} (h : a b) (ha : p a) :
p b
theorem succ.rec_iff {α : Type u_1} [preorder α] [succ_order α] {p : α → Prop} (hsucc : ∀ (a : α), p a p ) {a b : α} (h : a b) :
p a p b
@[protected, instance]
def order_dual.is_succ_archimedean {α : Type u_1} [preorder α] [pred_order α]  :
theorem has_le.le.exists_pred_iterate {α : Type u_1} [preorder α] [pred_order α] {a b : α} (h : a b) :
∃ (n : ),
theorem exists_pred_iterate_iff_le {α : Type u_1} [preorder α] [pred_order α] {a b : α} :
(∃ (n : ), = a) a b
theorem pred.rec {α : Type u_1} [preorder α] [pred_order α] {p : α → Prop} (hsucc : ∀ (a : α), p ap ) {a b : α} (h : b a) (ha : p a) :
p b
theorem pred.rec_iff {α : Type u_1} [preorder α] [pred_order α] {p : α → Prop} (hsucc : ∀ (a : α), p a p ) {a b : α} (h : a b) :
p a p b
theorem exists_succ_iterate_or {α : Type u_1} [linear_order α] [succ_order α] {a b : α} :
(∃ (n : ), = b) ∃ (n : ),
theorem succ.rec_linear {α : Type u_1} [linear_order α] [succ_order α] {p : α → Prop} (hsucc : ∀ (a : α), p a p ) (a b : α) :
p a p b
theorem exists_pred_iterate_or {α : Type u_1} [linear_order α] [pred_order α] {a b : α} :
(∃ (n : ), = a) ∃ (n : ),
theorem pred.rec_linear {α : Type u_1} [linear_order α] [pred_order α] {p : α → Prop} (hsucc : ∀ (a : α), p a p ) (a b : α) :
p a p b
theorem succ.rec_bot {α : Type u_1} [preorder α] [order_bot α] [succ_order α] (p : α → Prop) (hbot : p ) (hsucc : ∀ (a : α), p ap ) (a : α) :
p a
theorem pred.rec_top {α : Type u_1} [preorder α] [order_top α] [pred_order α] (p : α → Prop) (htop : p ) (hpred : ∀ (a : α), p ap ) (a : α) :
p a