mathlib documentation

order.succ_pred.basic

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

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 α) (h : succ_order.succ = succ_order.succ) :
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

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 α) (h : pred_order.pred = pred_order.pred) :
x = y
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
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 succ_order.of_core_succ {α : Type u_1} [linear_order α] (succ : α → α) (hn : ∀ {a : α}, ¬is_max a∀ (b : α), a < b succ a b) (hm : ∀ (a : α), is_max asucc a = a) (ᾰ : α) :
succ_order.succ = succ ᾰ
def succ_order.of_core {α : Type u_1} [linear_order α] (succ : α → α) (hn : ∀ {a : α}, ¬is_max a∀ (b : α), a < b succ a b) (hm : ∀ (a : α), is_max asucc 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 : α}, ¬is_min a∀ (b : α), b pred a b < a) (hm : ∀ (a : α), is_min apred 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 : α}, ¬is_min a∀ (b : α), b pred a b < a) (hm : ∀ (a : α), is_min apred a = a) (ᾰ : α) :
pred_order.pred = 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 : α) :
theorem order.max_of_succ_le {α : Type u_1} [preorder α] [succ_order α] {a : α} :
theorem order.succ_le_of_lt {α : Type u_1} [preorder α] [succ_order α] {a b : α} :
a < border.succ a b
theorem order.le_of_lt_succ {α : Type u_1} [preorder α] [succ_order α] {a b : α} :
a < order.succ ba b
@[simp]
theorem order.succ_le_iff_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} :
@[simp]
theorem order.lt_succ_iff_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} :
theorem order.lt_succ_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {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 : α) :
theorem order.covby_succ_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} (h : ¬is_max a) :
theorem order.lt_succ_iff_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬is_max a) :
theorem order.succ_le_iff_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬is_max a) :
theorem order.succ_lt_succ_iff_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬is_max a) (hb : ¬is_max b) :
theorem order.succ_le_succ_iff_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬is_max a) (hb : ¬is_max 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 : α) :
theorem order.Iio_succ_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} (ha : ¬is_max a) :
theorem order.Ici_succ_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} (ha : ¬is_max a) :
theorem order.Ico_succ_right_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (hb : ¬is_max b) :
theorem order.Ioo_succ_right_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (hb : ¬is_max b) :
theorem order.Icc_succ_left_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬is_max a) :
theorem order.Ico_succ_left_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬is_max a) :
theorem order.lt_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a : α) :
@[simp]
theorem order.lt_succ_iff {α : Type u_1} [preorder α] [succ_order α] {a b : α} [no_max_order α] :
@[simp]
theorem order.succ_le_iff {α : Type u_1} [preorder α] [succ_order α] {a b : α} [no_max_order α] :
theorem order.succ_le_succ_iff {α : Type u_1} [preorder α] [succ_order α] {a b : α} [no_max_order α] :
theorem order.succ_lt_succ_iff {α : Type u_1} [preorder α] [succ_order α] {a b : α} [no_max_order α] :
theorem order.le_of_succ_le_succ {α : Type u_1} [preorder α] [succ_order α] {a b : α} [no_max_order α] :

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 < border.succ a < order.succ 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 α] :
order.succ a < order.succ ba < b

Alias of the forward direction of order.succ_lt_succ_iff.

theorem order.covby_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (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 : α) :
@[simp]
theorem order.Ioo_succ_right {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a b : α) :
@[simp]
theorem order.Icc_succ_left {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a b : α) :
@[simp]
theorem order.Ico_succ_left {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a b : α) :
@[simp]
theorem order.succ_eq_iff_is_max {α : Type u_1} [partial_order α] [succ_order α] {a : α} :
theorem is_max.succ_eq {α : Type u_1} [partial_order α] [succ_order α] {a : α} :
is_max aorder.succ 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} [partial_order α] [succ_order α] {a b : α} (ha : ¬is_max a) (hb : ¬is_max b) :
theorem order.le_le_succ_iff {α : Type u_1} [partial_order α] [succ_order α] {a b : α} :
theorem covby.succ_eq {α : Type u_1} [partial_order α] [succ_order α] {a b : α} (h : a b) :
theorem order.le_succ_iff_eq_or_le {α : Type u_1} [partial_order α] [succ_order α] {a b : α} :
theorem order.lt_succ_iff_eq_or_lt_of_not_is_max {α : Type u_1} [partial_order α] [succ_order α] {a b : α} (hb : ¬is_max b) :
a < order.succ b a = b a < b
theorem order.Iic_succ {α : Type u_1} [partial_order α] [succ_order α] (a : α) :
theorem order.Icc_succ_right {α : Type u_1} [partial_order α] [succ_order α] {a b : α} (h : a order.succ b) :
theorem order.Ioc_succ_right {α : Type u_1} [partial_order α] [succ_order α] {a b : α} (h : a < order.succ b) :
theorem order.Ico_succ_right_eq_insert_of_not_is_max {α : Type u_1} [partial_order α] [succ_order α] {a b : α} (h₁ : a b) (h₂ : ¬is_max b) :
theorem order.Ioo_succ_right_eq_insert_of_not_is_max {α : Type u_1} [partial_order α] [succ_order α] {a b : α} (h₁ : a < b) (h₂ : ¬is_max b) :
@[simp]
theorem order.succ_eq_succ_iff {α : Type u_1} [partial_order α] [succ_order α] {a b : α} [no_max_order α] :
theorem order.succ_ne_succ_iff {α : Type u_1} [partial_order α] [succ_order α] {a b : α} [no_max_order α] :
theorem order.succ_ne_succ {α : Type u_1} [partial_order α] [succ_order α] {a b : α} [no_max_order α] :

Alias of the reverse direction of order.succ_ne_succ_iff.

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

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

theorem order.succ_eq_infi {α : Type u_1} [complete_lattice α] [succ_order α] (a : α) :
order.succ 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 : α) :
theorem order.min_of_le_pred {α : Type u_1} [preorder α] [pred_order α] {a : α} :
theorem order.le_pred_of_lt {α : Type u_1} [preorder α] [pred_order α] {a b : α} :
a < ba order.pred b
theorem order.le_of_pred_lt {α : Type u_1} [preorder α] [pred_order α] {a b : α} :
order.pred a < ba b
@[simp]
theorem order.le_pred_iff_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} :
@[simp]
theorem order.pred_lt_iff_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} :
theorem order.pred_lt_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {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 : α) :
theorem order.pred_covby_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} (h : ¬is_min a) :
theorem order.pred_lt_iff_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬is_min a) :
theorem order.le_pred_iff_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬is_min 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 : α) :
theorem order.Ioi_pred_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} (ha : ¬is_min a) :
theorem order.Iic_pred_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} (ha : ¬is_min a) :
theorem order.Ioc_pred_left_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬is_min a) :
theorem order.Ioo_pred_left_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬is_min a) :
theorem order.Icc_pred_right_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬is_min b) :
theorem order.Ioc_pred_right_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬is_min b) :
theorem order.pred_lt {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a : α) :
@[simp]
theorem order.pred_lt_iff {α : Type u_1} [preorder α] [pred_order α] {a b : α} [no_min_order α] :
@[simp]
theorem order.le_pred_iff {α : Type u_1} [preorder α] [pred_order α] {a b : α} [no_min_order α] :
theorem order.pred_le_pred_iff {α : Type u_1} [preorder α] [pred_order α] {a b : α} [no_min_order α] :
theorem order.pred_lt_pred_iff {α : Type u_1} [preorder α] [pred_order α] {a b : α} [no_min_order α] :
theorem order.le_of_pred_le_pred {α : Type u_1} [preorder α] [pred_order α] {a b : α} [no_min_order α] :

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 < border.pred a < order.pred 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 α] :
order.pred a < order.pred ba < b

Alias of the forward direction of order.pred_lt_pred_iff.

theorem order.pred_covby {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (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 : α) :
@[simp]
theorem order.Ioo_pred_left {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a b : α) :
@[simp]
theorem order.Icc_pred_right {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a b : α) :
@[simp]
theorem order.Ioc_pred_right {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a b : α) :
@[simp]
theorem order.pred_eq_iff_is_min {α : Type u_1} [partial_order α] [pred_order α] {a : α} :
theorem is_min.pred_eq {α : Type u_1} [partial_order α] [pred_order α] {a : α} :
is_min aorder.pred a = a

Alias of the reverse direction of order.pred_eq_iff_is_min.

theorem order.pred_le_le_iff {α : Type u_1} [partial_order α] [pred_order α] {a b : α} :
theorem covby.pred_eq {α : Type u_1} [partial_order α] [pred_order α] {a b : α} (h : a b) :
theorem order.pred_le_iff_eq_or_le {α : Type u_1} [partial_order α] [pred_order α] {a b : α} :
theorem order.pred_lt_iff_eq_or_lt_of_not_is_min {α : Type u_1} [partial_order α] [pred_order α] {a b : α} (ha : ¬is_min a) :
order.pred a < b a = b a < b
theorem order.Ici_pred {α : Type u_1} [partial_order α] [pred_order α] (a : α) :
theorem order.Icc_pred_left {α : Type u_1} [partial_order α] [pred_order α] {a b : α} (h : order.pred a b) :
theorem order.Ico_pred_left {α : Type u_1} [partial_order α] [pred_order α] {a b : α} (h : order.pred a < b) :
@[simp]
theorem order.pred_eq_pred_iff {α : Type u_1} [partial_order α] [pred_order α] {a b : α} [no_min_order α] :
theorem order.pred_ne_pred_iff {α : Type u_1} [partial_order α] [pred_order α] {a b : α} [no_min_order α] :
theorem order.pred_ne_pred {α : Type u_1} [partial_order α] [pred_order α] {a b : α} [no_min_order α] :

Alias of the reverse direction of order.pred_ne_pred_iff.

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

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

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

Successor-predecessor orders #

@[simp]
theorem order.succ_pred_of_not_is_min {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] {a : α} (h : ¬is_min a) :
@[simp]
theorem order.pred_succ_of_not_is_max {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] {a : α} (h : ¬is_max a) :
@[simp]
theorem order.succ_pred {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] [no_min_order α] (a : α) :
@[simp]
theorem order.pred_succ {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] [no_max_order α] (a : α) :

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
@[simp]
theorem with_top.succ_coe_top {α : Type u_1} [decidable_eq α] [partial_order α] [order_top α] [succ_order α] :
theorem with_top.succ_coe_of_ne_top {α : Type u_1} [decidable_eq α] [partial_order α] [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 : α) :

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]
def with_top.pred_order.is_empty {α : Type u_1} [preorder α] [no_max_order α] [hα : nonempty α] :

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 : α) :
@[protected, instance]
def with_bot.pred_order {α : Type u_1} [decidable_eq α] [partial_order α] [order_bot α] [pred_order α] :
Equations
@[simp]
theorem with_bot.pred_coe_bot {α : Type u_1} [decidable_eq α] [partial_order α] [order_bot α] [pred_order α] :
theorem with_bot.pred_coe_of_ne_bot {α : Type u_1} [decidable_eq α] [partial_order α] [order_bot α] [pred_order α] {a : α} (h : a ) :

Adding a to a no_min_order #

@[protected, instance]
def with_bot.succ_order.is_empty {α : Type u_1} [preorder α] [no_min_order α] [hα : nonempty α] :
@[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 α] [is_succ_archimedean α] {a b : α} (h : a b) :
∃ (n : ), order.succ^[n] a = b
theorem exists_succ_iterate_iff_le {α : Type u_1} [preorder α] [succ_order α] [is_succ_archimedean α] {a b : α} :
(∃ (n : ), order.succ^[n] a = b) a b
theorem succ.rec {α : Type u_1} [preorder α] [succ_order α] [is_succ_archimedean α] {P : α → Prop} {m : α} (h0 : P m) (h1 : ∀ (n : α), m nP nP (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 α] [is_succ_archimedean α] {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 α] [is_pred_archimedean α] {a b : α} (h : a b) :
∃ (n : ), order.pred^[n] b = a
theorem exists_pred_iterate_iff_le {α : Type u_1} [preorder α] [pred_order α] [is_pred_archimedean α] {a b : α} :
(∃ (n : ), order.pred^[n] b = a) a b
theorem pred.rec {α : Type u_1} [preorder α] [pred_order α] [is_pred_archimedean α] {P : α → Prop} {m : α} (h0 : P m) (h1 : ∀ (n : α), n mP nP (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 α] [is_pred_archimedean α] {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 α] [is_succ_archimedean α] {a b : α} :
(∃ (n : ), order.succ^[n] a = b) ∃ (n : ), 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 (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 : ), order.pred^[n] b = a) ∃ (n : ), 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 (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 α] [is_succ_archimedean α] (p : α → Prop) (hbot : p ) (hsucc : ∀ (a : α), p ap (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 (order.pred a)) (a : α) :
p a