mathlib3documentation

order.succ_pred.basic

Successor and predecessor #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• `succ_order`: Order equipped with a sensible successor function.
• `pred_order`: Order equipped with a sensible predecessor function.
• `is_succ_archimedean`: `succ_order` where `succ` iterated to an element gives all the greater ones.
• `is_pred_archimedean`: `pred_order` 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 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 `max_of_succ_le`). The stricter condition of every element having a sensible successor can be obtained through the combination of `succ_order α` and `no_max_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)
``````

`covby` should help here.

@[ext, class]
structure succ_order (α : Type u_2) [preorder α] :
Type u_2
• succ : α α
• le_succ : (a : α),
• max_of_succ_le : {a : α},
• succ_le_of_lt : {a b : α}, a < b
• le_of_lt_succ : {a b : α}, a b

Order equipped with a sensible successor function.

Instances of this typeclass
Instances of other typeclasses for `succ_order`
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 α) :
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 : α),
• min_of_le_pred : {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 of this typeclass
Instances of other typeclasses for `pred_order`
theorem pred_order.ext {α : Type u_2} {_inst_1 : preorder α} (x y : pred_order α)  :
x = y
@[protected, instance]
def order_dual.pred_order {α : Type u_1} [preorder α] [succ_order α] :
Equations
@[protected, instance]
def order_dual.succ_order {α : Type u_1} [preorder α] [pred_order α] :
Equations
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 b a b) :

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

Equations
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 < b a b) :

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

Equations
@[simp]
theorem succ_order.of_core_succ {α : Type u_1} [linear_order α] (succ : α α) (hn : {a : α}, ¬ (b : α), a < b succ a b) (hm : (a : α), succ a = a) (ᾰ : α) :
= succ ᾰ
def succ_order.of_core {α : Type u_1} [linear_order α] (succ : α α) (hn : {a : α}, ¬ (b : α), a < b succ a b) (hm : (a : α), succ a = a) :

A constructor for `succ_order α` for `α` a linear order.

Equations
def pred_order.of_core {α : Type u_1} [linear_order α] (pred : α α) (hn : {a : α}, ¬ (b : α), b pred a b < a) (hm : (a : α), pred a = a) :

A constructor for `pred_order α` for `α` a linear order.

Equations
@[simp]
theorem pred_order.of_core_pred {α : Type u_1} [linear_order α] (pred : α α) (hn : {a : α}, ¬ (b : α), b pred a b < a) (hm : (a : α), pred a = a) (ᾰ : α) :
= pred ᾰ
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
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 minimal element.

Equations

Successor order #

def order.succ {α : Type u_1} [preorder α] [succ_order α] :
α α

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
theorem order.le_succ {α : Type u_1} [preorder α] [succ_order α] (a : α) :
a
theorem order.max_of_succ_le {α : Type u_1} [preorder α] [succ_order α] {a : α} :
a
theorem order.succ_le_of_lt {α : Type u_1} [preorder α] [succ_order α] {a b : α} :
a < b b
theorem order.le_of_lt_succ {α : Type u_1} [preorder α] [succ_order α] {a b : α} :
a < a b
@[simp]
theorem order.succ_le_iff_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} :
a
@[simp]
theorem order.lt_succ_iff_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} :
a < ¬
theorem order.lt_succ_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} :
¬ a <

Alias of the reverse direction of `order.lt_succ_iff_not_is_max`.

theorem order.wcovby_succ {α : Type u_1} [preorder α] [succ_order α] (a : α) :
a ⩿
theorem order.covby_succ_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} (h : ¬) :
a
theorem order.lt_succ_iff_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬) :
b < b a
theorem order.succ_le_iff_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬) :
b a < b
theorem order.succ_lt_succ_iff_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬) (hb : ¬) :
a < b
theorem order.succ_le_succ_iff_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬) (hb : ¬) :
a b
@[simp]
theorem order.succ_le_succ {α : Type u_1} [preorder α] [succ_order α] {a b : α} (h : a b) :
theorem order.succ_mono {α : Type u_1} [preorder α] [succ_order α] :
theorem order.le_succ_iterate {α : Type u_1} [preorder α] [succ_order α] (k : ) (x : α) :
x
theorem order.is_max_iterate_succ_of_eq_of_lt {α : Type u_1} [preorder α] [succ_order α] {a : α} {n m : } (h_eq : = ) (h_lt : n < m) :
theorem order.is_max_iterate_succ_of_eq_of_ne {α : Type u_1} [preorder α] [succ_order α] {a : α} {n m : } (h_eq : = ) (h_ne : n m) :
theorem order.Iio_succ_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} (ha : ¬) :
=
theorem order.Ici_succ_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} (ha : ¬) :
=
theorem order.Ico_succ_right_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (hb : ¬) :
(order.succ b) = b
theorem order.Ioo_succ_right_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (hb : ¬) :
(order.succ b) = b
theorem order.Icc_succ_left_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬) :
b = b
theorem order.Ico_succ_left_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬) :
b = b
theorem order.lt_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a : α) :
a <
@[simp]
theorem order.lt_succ_iff {α : Type u_1} [preorder α] [succ_order α] {a b : α} [no_max_order α] :
a < a b
@[simp]
theorem order.succ_le_iff {α : Type u_1} [preorder α] [succ_order α] {a b : α} [no_max_order α] :
b a < b
theorem order.succ_le_succ_iff {α : Type u_1} [preorder α] [succ_order α] {a b : α} [no_max_order α] :
a b
theorem order.succ_lt_succ_iff {α : Type u_1} [preorder α] [succ_order α] {a b : α} [no_max_order α] :
a < b
theorem order.le_of_succ_le_succ {α : Type u_1} [preorder α] [succ_order α] {a b : α} [no_max_order α] :
a b

Alias of the forward direction of `order.succ_le_succ_iff`.

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

Alias of the reverse direction of `order.succ_lt_succ_iff`.

theorem order.lt_of_succ_lt_succ {α : Type u_1} [preorder α] [succ_order α] {a b : α} [no_max_order α] :
a < b

Alias of the forward direction of `order.succ_lt_succ_iff`.

theorem order.succ_strict_mono {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] :
theorem order.covby_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a : α) :
a
@[simp]
theorem order.Iio_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a : α) :
=
@[simp]
theorem order.Ici_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a : α) :
=
@[simp]
theorem order.Ico_succ_right {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a b : α) :
(order.succ b) = b
@[simp]
theorem order.Ioo_succ_right {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a b : α) :
(order.succ b) = b
@[simp]
theorem order.Icc_succ_left {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a b : α) :
b = b
@[simp]
theorem order.Ico_succ_left {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a b : α) :
b = b
@[simp]
theorem order.succ_eq_iff_is_max {α : Type u_1} [succ_order α] {a : α} :
= a
theorem is_max.succ_eq {α : Type u_1} [succ_order α] {a : α} :
= a

Alias of the reverse direction of `order.succ_eq_iff_is_max`.

theorem order.succ_eq_succ_iff_of_not_is_max {α : Type u_1} [succ_order α] {a b : α} (ha : ¬) (hb : ¬) :
a = b
theorem order.le_le_succ_iff {α : Type u_1} [succ_order α] {a b : α} :
a b b b = a b =
theorem covby.succ_eq {α : Type u_1} [succ_order α] {a b : α} (h : a b) :
= b
theorem wcovby.le_succ {α : Type u_1} [succ_order α] {a b : α} (h : a ⩿ b) :
b
theorem order.le_succ_iff_eq_or_le {α : Type u_1} [succ_order α] {a b : α} :
a a = a b
theorem order.lt_succ_iff_eq_or_lt_of_not_is_max {α : Type u_1} [succ_order α] {a b : α} (hb : ¬) :
a < a = b a < b
theorem order.Iic_succ {α : Type u_1} [succ_order α] (a : α) :
= (set.Iic a)
theorem order.Icc_succ_right {α : Type u_1} [succ_order α] {a b : α} (h : a ) :
(order.succ b) = (set.Icc a b)
theorem order.Ioc_succ_right {α : Type u_1} [succ_order α] {a b : α} (h : a < ) :
(order.succ b) = (set.Ioc a b)
theorem order.Iio_succ_eq_insert_of_not_is_max {α : Type u_1} [succ_order α] {a : α} (h : ¬) :
= (set.Iio a)
theorem order.Ico_succ_right_eq_insert_of_not_is_max {α : Type u_1} [succ_order α] {a b : α} (h₁ : a b) (h₂ : ¬) :
(order.succ b) = (set.Ico a b)
theorem order.Ioo_succ_right_eq_insert_of_not_is_max {α : Type u_1} [succ_order α] {a b : α} (h₁ : a < b) (h₂ : ¬) :
(order.succ b) = (set.Ioo a b)
@[simp]
theorem order.succ_eq_succ_iff {α : Type u_1} [succ_order α] {a b : α} [no_max_order α] :
a = b
theorem order.succ_injective {α : Type u_1} [succ_order α] [no_max_order α] :
theorem order.succ_ne_succ_iff {α : Type u_1} [succ_order α] {a b : α} [no_max_order α] :
a b
theorem order.succ_ne_succ {α : Type u_1} [succ_order α] {a b : α} [no_max_order α] :
a b

Alias of the reverse direction of `order.succ_ne_succ_iff`.

theorem order.lt_succ_iff_eq_or_lt {α : Type u_1} [succ_order α] {a b : α} [no_max_order α] :
a < a = b a < b
theorem order.succ_eq_iff_covby {α : Type u_1} [succ_order α] {a b : α} [no_max_order α] :
= b a b
theorem order.Iio_succ_eq_insert {α : Type u_1} [succ_order α] [no_max_order α] (a : α) :
= (set.Iio a)
theorem order.Ico_succ_right_eq_insert {α : Type u_1} [succ_order α] {a b : α} [no_max_order α] (h : a b) :
(order.succ b) = (set.Ico a b)
theorem order.Ioo_succ_right_eq_insert {α : Type u_1} [succ_order α] {a b : α} [no_max_order α] (h : a < b) :
(order.succ b) = (set.Ioo a b)
@[simp]
theorem order.succ_top {α : Type u_1} [succ_order α] [order_top α] :
@[simp]
theorem order.succ_le_iff_eq_top {α : Type u_1} [succ_order α] {a : α} [order_top α] :
a a =
@[simp]
theorem order.lt_succ_iff_ne_top {α : Type u_1} [succ_order α] {a : α} [order_top α] :
a < a
@[simp]
theorem order.lt_succ_bot_iff {α : Type u_1} [succ_order α] {a : α} [order_bot α] [no_max_order α] :
a =
theorem order.le_succ_bot_iff {α : Type u_1} [succ_order α] {a : α} [order_bot α] :
a =
theorem order.bot_lt_succ {α : Type u_1} [succ_order α] [order_bot α] [nontrivial α] (a : α) :
theorem order.succ_ne_bot {α : Type u_1} [succ_order α] [order_bot α] [nontrivial α] (a : α) :
@[protected, instance]
def order.succ_order.subsingleton {α : Type u_1}  :

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

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

Predecessor order #

def order.pred {α : Type u_1} [preorder α] [pred_order α] :
α α

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
theorem order.pred_le {α : Type u_1} [preorder α] [pred_order α] (a : α) :
a
theorem order.min_of_le_pred {α : Type u_1} [preorder α] [pred_order α] {a : α} :
a
theorem order.le_pred_of_lt {α : Type u_1} [preorder α] [pred_order α] {a b : α} :
a < b a
theorem order.le_of_pred_lt {α : Type u_1} [preorder α] [pred_order α] {a b : α} :
< b a b
@[simp]
theorem order.le_pred_iff_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} :
a
@[simp]
theorem order.pred_lt_iff_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} :
< a ¬
theorem order.pred_lt_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} :
¬ < a

Alias of the reverse direction of `order.pred_lt_iff_not_is_min`.

theorem order.pred_wcovby {α : Type u_1} [preorder α] [pred_order α] (a : α) :
⩿ a
theorem order.pred_covby_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} (h : ¬) :
a
theorem order.pred_lt_iff_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬) :
< b a b
theorem order.le_pred_iff_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬) :
b b < a
@[simp]
theorem order.pred_le_pred {α : Type u_1} [preorder α] [pred_order α] {a b : α} (h : a b) :
theorem order.pred_mono {α : Type u_1} [preorder α] [pred_order α] :
theorem order.pred_iterate_le {α : Type u_1} [preorder α] [pred_order α] (k : ) (x : α) :
x
theorem order.is_min_iterate_pred_of_eq_of_lt {α : Type u_1} [preorder α] [pred_order α] {a : α} {n m : } (h_eq : = ) (h_lt : n < m) :
theorem order.is_min_iterate_pred_of_eq_of_ne {α : Type u_1} [preorder α] [pred_order α] {a : α} {n m : } (h_eq : = ) (h_ne : n m) :
theorem order.Ioi_pred_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} (ha : ¬) :
=
theorem order.Iic_pred_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} (ha : ¬) :
=
theorem order.Ioc_pred_left_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬) :
b = b
theorem order.Ioo_pred_left_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬) :
b = b
theorem order.Icc_pred_right_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬) :
(order.pred b) = b
theorem order.Ioc_pred_right_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬) :
(order.pred b) = b
theorem order.pred_lt {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a : α) :
< a
@[simp]
theorem order.pred_lt_iff {α : Type u_1} [preorder α] [pred_order α] {a b : α} [no_min_order α] :
< b a b
@[simp]
theorem order.le_pred_iff {α : Type u_1} [preorder α] [pred_order α] {a b : α} [no_min_order α] :
a a < b
theorem order.pred_le_pred_iff {α : Type u_1} [preorder α] [pred_order α] {a b : α} [no_min_order α] :
a b
theorem order.pred_lt_pred_iff {α : Type u_1} [preorder α] [pred_order α] {a b : α} [no_min_order α] :
a < b
theorem order.le_of_pred_le_pred {α : Type u_1} [preorder α] [pred_order α] {a b : α} [no_min_order α] :
a b

Alias of the forward direction of `order.pred_le_pred_iff`.

theorem order.pred_lt_pred {α : Type u_1} [preorder α] [pred_order α] {a b : α} [no_min_order α] :
a < b

Alias of the reverse direction of `order.pred_lt_pred_iff`.

theorem order.lt_of_pred_lt_pred {α : Type u_1} [preorder α] [pred_order α] {a b : α} [no_min_order α] :
a < b

Alias of the forward direction of `order.pred_lt_pred_iff`.

theorem order.pred_strict_mono {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] :
theorem order.pred_covby {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a : α) :
a
@[simp]
theorem order.Ioi_pred {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a : α) :
=
@[simp]
theorem order.Iic_pred {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a : α) :
=
@[simp]
theorem order.Ioc_pred_left {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a b : α) :
b = b
@[simp]
theorem order.Ioo_pred_left {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a b : α) :
b = b
@[simp]
theorem order.Icc_pred_right {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a b : α) :
(order.pred b) = b
@[simp]
theorem order.Ioc_pred_right {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a b : α) :
(order.pred b) = b
@[simp]
theorem order.pred_eq_iff_is_min {α : Type u_1} [pred_order α] {a : α} :
= a
theorem is_min.pred_eq {α : Type u_1} [pred_order α] {a : α} :
= a

Alias of the reverse direction of `order.pred_eq_iff_is_min`.

theorem order.pred_le_le_iff {α : Type u_1} [pred_order α] {a b : α} :
b b a b = a b =
theorem covby.pred_eq {α : Type u_1} [pred_order α] {a b : α} (h : a b) :
= a
theorem wcovby.pred_le {α : Type u_1} [pred_order α] {a b : α} (h : a ⩿ b) :
a
theorem order.pred_le_iff_eq_or_le {α : Type u_1} [pred_order α] {a b : α} :
b b = a b
theorem order.pred_lt_iff_eq_or_lt_of_not_is_min {α : Type u_1} [pred_order α] {a b : α} (ha : ¬) :
< b a = b a < b
theorem order.Ici_pred {α : Type u_1} [pred_order α] (a : α) :
= (set.Ici a)
theorem order.Ioi_pred_eq_insert_of_not_is_min {α : Type u_1} [pred_order α] {a : α} (ha : ¬) :
= (set.Ioi a)
theorem order.Icc_pred_left {α : Type u_1} [pred_order α] {a b : α} (h : b) :
b = (set.Icc a b)
theorem order.Ico_pred_left {α : Type u_1} [pred_order α] {a b : α} (h : < b) :
b = (set.Ico a b)
@[simp]
theorem order.pred_eq_pred_iff {α : Type u_1} [pred_order α] {a b : α} [no_min_order α] :
a = b
theorem order.pred_injective {α : Type u_1} [pred_order α] [no_min_order α] :
theorem order.pred_ne_pred_iff {α : Type u_1} [pred_order α] {a b : α} [no_min_order α] :
a b
theorem order.pred_ne_pred {α : Type u_1} [pred_order α] {a b : α} [no_min_order α] :
a b

Alias of the reverse direction of `order.pred_ne_pred_iff`.

theorem order.pred_lt_iff_eq_or_lt {α : Type u_1} [pred_order α] {a b : α} [no_min_order α] :
< b a = b a < b
theorem order.pred_eq_iff_covby {α : Type u_1} [pred_order α] {a b : α} [no_min_order α] :
= a a b
theorem order.Ioi_pred_eq_insert {α : Type u_1} [pred_order α] [no_min_order α] (a : α) :
= (set.Ioi a)
theorem order.Ico_pred_right_eq_insert {α : Type u_1} [pred_order α] {a b : α} [no_min_order α] (h : a b) :
b = (set.Ioc a b)
theorem order.Ioo_pred_right_eq_insert {α : Type u_1} [pred_order α] {a b : α} [no_min_order α] (h : a < b) :
b = (set.Ioo a b)
@[simp]
theorem order.pred_bot {α : Type u_1} [pred_order α] [order_bot α] :
@[simp]
theorem order.le_pred_iff_eq_bot {α : Type u_1} [pred_order α] {a : α} [order_bot α] :
a a =
@[simp]
theorem order.pred_lt_iff_ne_bot {α : Type u_1} [pred_order α] {a : α} [order_bot α] :
< a a
@[simp]
theorem order.pred_top_lt_iff {α : Type u_1} [pred_order α] {a : α} [order_top α] [no_min_order α] :
a =
theorem order.pred_top_le_iff {α : Type u_1} [pred_order α] {a : α} [order_top α] :
a =
theorem order.pred_lt_top {α : Type u_1} [pred_order α] [order_top α] [nontrivial α] (a : α) :
theorem order.pred_ne_top {α : Type u_1} [pred_order α] [order_top α] [nontrivial α] (a : α) :
@[protected, instance]
def order.pred_order.subsingleton {α : Type u_1}  :

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

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

Successor-predecessor orders #

@[simp]
theorem order.succ_pred_of_not_is_min {α : Type u_1} [succ_order α] [pred_order α] {a : α} (h : ¬) :
= a
@[simp]
theorem order.pred_succ_of_not_is_max {α : Type u_1} [succ_order α] [pred_order α] {a : α} (h : ¬) :
= a
@[simp]
theorem order.succ_pred {α : Type u_1} [succ_order α] [pred_order α] [no_min_order α] (a : α) :
= a
@[simp]
theorem order.pred_succ {α : Type u_1} [succ_order α] [pred_order α] [no_max_order α] (a : α) :
= a
theorem order.pred_succ_iterate_of_not_is_max {α : Type u_1} [succ_order α] [pred_order α] (i : α) (n : ) (hin : ¬is_max (order.succ^[n - 1] i)) :
= i
theorem order.succ_pred_iterate_of_not_is_min {α : Type u_1} [succ_order α] [pred_order α] (i : α) (n : ) (hin : ¬is_min (order.pred^[n - 1] i)) :
= i

`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_max_order`: Preserves `succ`. Never preserves `pred`.
• Adding a `⊥` to an `order_bot`: Preserves `succ` and `pred`.
• Adding a `⊥` to a `no_min_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
@[simp]
theorem with_top.succ_coe_top {α : Type u_1} [decidable_eq α] [order_top α] [succ_order α] :
theorem with_top.succ_coe_of_ne_top {α : Type u_1} [decidable_eq α] [order_top α] [succ_order α] {a : α} (h : a ) :
@[protected, instance]
def with_top.pred_order {α : Type u_1} [preorder α] [order_top α] [pred_order α] :
Equations
@[simp]
theorem with_top.pred_top {α : Type u_1} [preorder α] [order_top α] [pred_order α] :
@[simp]
theorem with_top.pred_coe {α : Type u_1} [preorder α] [order_top α] [pred_order α] (a : α) :
@[simp]
theorem with_top.pred_untop {α : Type u_1} [preorder α] [order_top α] [pred_order α] (a : with_top α) (ha : a ) :

Adding a `⊤` to a `no_max_order`#

@[protected, instance]
Equations
@[simp]
theorem with_top.succ_coe {α : Type u_1} [preorder α] [no_max_order α] [succ_order α] (a : α) :
@[protected, instance]

Adding a `⊥` to an `order_bot`#

@[protected, instance]
def with_bot.succ_order {α : Type u_1} [preorder α] [order_bot α] [succ_order α] :
Equations
@[simp]
theorem with_bot.succ_bot {α : Type u_1} [preorder α] [order_bot α] [succ_order α] :
@[simp]
theorem with_bot.succ_coe {α : Type u_1} [preorder α] [order_bot α] [succ_order α] (a : α) :
@[simp]
theorem with_bot.succ_unbot {α : Type u_1} [preorder α] [order_bot α] [succ_order α] (a : with_bot α) (ha : a ) :
@[protected, instance]
def with_bot.pred_order {α : Type u_1} [decidable_eq α] [order_bot α] [pred_order α] :
Equations
@[simp]
theorem with_bot.pred_coe_bot {α : Type u_1} [decidable_eq α] [order_bot α] [pred_order α] :
theorem with_bot.pred_coe_of_ne_bot {α : Type u_1} [decidable_eq α] [order_bot α] [pred_order α] {a : α} (h : a ) :

Adding a `⊥` to a `no_min_order`#

@[protected, instance]
@[protected, instance]
Equations
@[simp]
theorem with_bot.pred_coe {α : Type u_1} [preorder α] [no_min_order α] [pred_order α] (a : α) :

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 of this typeclass
@[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 of this typeclass
@[protected, instance]
theorem has_le.le.exists_succ_iterate {α : Type u_1} [preorder α] [succ_order α] {a b : α} (h : a b) :
(n : ), = b
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} {m : α} (h0 : P m) (h1 : (n : α), m n P n P (order.succ n)) ⦃n : α⦄ (hmn : m n) :
P n

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

theorem succ.rec_iff {α : Type u_1} [preorder α] [succ_order α] {p : α Prop} (hsucc : (a : α), p a p (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 α] {a b : α} (h : a b) :
(n : ), = a
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} {m : α} (h0 : P m) (h1 : (n : α), n m P n P (order.pred n)) ⦃n : α⦄ (hmn : n m) :
P n

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

theorem pred.rec_iff {α : Type u_1} [preorder α] [pred_order α] {p : α Prop} (hsucc : (a : α), p a p (order.pred a)) {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 : ), = a
theorem succ.rec_linear {α : Type u_1} [linear_order α] [succ_order α] {p : α Prop} (hsucc : (a : α), p a p (order.succ a)) (a b : α) :
p a p b
theorem exists_pred_iterate_or {α : Type u_1} [linear_order α] [pred_order α] {a b : α} :
( (n : ), = a) (n : ), = b
theorem pred.rec_linear {α : Type u_1} [linear_order α] [pred_order α] {p : α Prop} (hsucc : (a : α), p a p (order.pred a)) (a b : α) :
p a p b
@[protected, instance]
@[protected, instance]
theorem succ.rec_bot {α : Type u_1} [preorder α] [order_bot α] [succ_order α] (p : α Prop) (hbot : p ) (hsucc : (a : α), p a p (order.succ a)) (a : α) :
p a
theorem pred.rec_top {α : Type u_1} [preorder α] [order_top α] [pred_order α] (p : α Prop) (htop : p ) (hpred : (a : α), p a p (order.pred a)) (a : α) :
p a