mathlib documentation

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

Typeclasses #

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

Order equipped with a sensible successor function.

Instances
theorem succ_order.ext {α : Type u_2} {_inst_1 : preorder α} (x y : succ_order α) (h : succ_order.succ = succ_order.succ) :
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.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 : α} :
theorem succ_order.succ_le_iff {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] {a b : α} :
@[simp]
theorem succ_order.succ_le_succ_iff {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] {a b : α} :
theorem le_of_succ_le_succ {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] {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 : α} :
theorem succ_lt_succ {α : Type u_1} [preorder α] [succ_order α] [no_top_order α] {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 : α} :

Alias of succ_lt_succ_iff.

@[protected, instance]

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

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

Alias of succ_ne_succ_iff.

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

Alias of succ_ne_succ_iff.

theorem succ_order.lt_succ_iff_lt_or_eq {α : Type u_1} [partial_order α] [succ_order α] [no_top_order α] {a b : α} :
a < succ_order.succ b a < b a = b
theorem succ_order.le_succ_iff_lt_or_eq {α : Type u_1} [partial_order α] [succ_order α] [no_top_order α] {a b : α} :
@[simp]
theorem succ_order.succ_top {α : Type u_1} [partial_order α] [order_top α] [succ_order α] :
@[simp]
theorem succ_order.succ_le_iff_eq_top {α : Type u_1} [partial_order α] [order_top α] [succ_order α] {a : α} :
@[simp]
theorem succ_order.lt_succ_iff_ne_top {α : Type u_1} [partial_order α] [order_top α] [succ_order α] {a : α} :
theorem succ_order.bot_lt_succ {α : Type u_1} [partial_order α] [order_bot α] [succ_order α] [nontrivial α] (a : α) :
theorem succ_order.succ_ne_bot {α : Type u_1} [partial_order α] [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} [complete_lattice α] [succ_order α] (a : α) :
succ_order.succ 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

Order equipped with a sensible predecessor function.

Instances
theorem pred_order.ext {α : Type u_2} {_inst_1 : preorder α} (x y : pred_order α) (h : pred_order.pred = pred_order.pred) :
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_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 : α} :
theorem pred_order.le_pred_iff {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] {a b : α} :
@[simp]
theorem pred_order.pred_le_pred_iff {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] {a b : α} :
theorem le_of_pred_le_pred {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] {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 : α} :
theorem pred_lt_pred {α : Type u_1} [preorder α] [pred_order α] [no_bot_order α] {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 : α} :

Alias of pred_lt_pred_iff.

@[protected, instance]

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

theorem pred_order.pred_le_le_iff {α : Type u_1} [partial_order α] [pred_order α] {a b : α} :
theorem pred_order.pred_eq_pred_iff {α : Type u_1} [partial_order α] [pred_order α] [no_bot_order α] {a b : α} :
theorem pred_order.pred_ne_pred_iff {α : Type u_1} [partial_order α] [pred_order α] [no_bot_order α] {a b : α} :
theorem pred_order.pred_lt_iff_lt_or_eq {α : Type u_1} [partial_order α] [pred_order α] [no_bot_order α] {a b : α} :
pred_order.pred a < b a < b a = b
theorem pred_order.le_pred_iff_lt_or_eq {α : Type u_1} [partial_order α] [pred_order α] [no_bot_order α] {a b : α} :
@[simp]
theorem pred_order.pred_bot {α : Type u_1} [partial_order α] [order_bot α] [pred_order α] :
@[simp]
theorem pred_order.le_pred_iff_eq_bot {α : Type u_1} [partial_order α] [order_bot α] [pred_order α] {a : α} :
@[simp]
theorem pred_order.pred_lt_iff_ne_bot {α : Type u_1} [partial_order α] [order_bot α] [pred_order α] {a : α} :
theorem pred_order.pred_lt_top {α : Type u_1} [partial_order α] [order_top α] [pred_order α] [nontrivial α] (a : α) :
theorem pred_order.pred_ne_top {α : Type u_1} [partial_order α] [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} [complete_lattice α] [pred_order α] (a : α) :
pred_order.pred 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 #

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

Adding a to a no_top_order #

@[protected, instance]
def of_no_top {α : Type u_1} [partial_order α] [no_top_order α] [succ_order α] :
Equations
@[protected, instance]
def pred_order.is_empty {α : Type u_1} [partial_order α] [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 α] [partial_order α] [order_bot α] [pred_order α] :
Equations

Adding a to a no_bot_order #

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

Archimedeanness #

@[class]
structure is_succ_archimedean (α : Type u_2) [preorder α] [succ_order α] :
Prop

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

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

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