mathlib3 documentation

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 : α), a ≤ succ_order.succ a
max_of_succ_le : ∀ {a : α}, succ_order.succ a ≤ a → is_max a
succ_le_of_lt : ∀ {a b : α}, a < b → succ_order.succ a ≤ b
le_of_lt_succ : ∀ {a b : α}, a < succ_order.succ 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 α) (h : succ_order.succ = succ_order.succ) :

x = y

theorem succ_order.ext_iff {α : Type u_2} {_inst_1 : preorder α} (x y : succ_order α) :

x = y ↔ succ_order.succ = succ_order.succ

theorem pred_order.ext_iff {α : Type u_2} {_inst_1 : preorder α} (x y : pred_order α) :

x = y ↔ pred_order.pred = pred_order.pred

@[ext, class]

structure pred_order (α : Type u_2) [preorder α] :

Type u_2

pred : α → α
pred_le : ∀ (a : α), pred_order.pred a ≤ a
min_of_le_pred : ∀ {a : α}, a ≤ pred_order.pred a → is_min a
le_pred_of_lt : ∀ {a b : α}, a < b → a ≤ pred_order.pred b
le_of_pred_lt : ∀ {a b : α}, pred_order.pred 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 α) (h : pred_order.pred = pred_order.pred) :

x = y

@[protected, instance]

def order_dual.pred_order {α : Type u_1} [preorder α] [succ_order α] :

pred_order αᵒᵈ

Equations

order_dual.pred_order = {pred := ⇑order_dual.to_dual ∘ succ_order.succ ∘ ⇑order_dual.of_dual, pred_le := _, min_of_le_pred := _, le_pred_of_lt := _, le_of_pred_lt := _}

@[protected, instance]

def order_dual.succ_order {α : Type u_1} [preorder α] [pred_order α] :

succ_order αᵒᵈ

Equations

order_dual.succ_order = {succ := ⇑order_dual.to_dual ∘ pred_order.pred ∘ ⇑order_dual.of_dual, le_succ := _, max_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}

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

succ_order.of_succ_le_iff_of_le_lt_succ succ hsucc_le_iff hle_of_lt_succ = {succ := succ, le_succ := _, max_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}

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

pred_order.of_le_pred_iff_of_pred_le_pred pred hle_pred_iff hle_of_pred_lt = {pred := pred, pred_le := _, min_of_le_pred := _, le_pred_of_lt := _, le_of_pred_lt := _}

@[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 a → succ 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 a → succ a = a) :

A constructor for succ_order α for α a linear order.

Equations

succ_order.of_core succ hn hm = {succ := succ, le_succ := _, max_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}

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 a → pred a = a) :

A constructor for pred_order α for α a linear order.

Equations

pred_order.of_core pred hn hm = {pred := pred, pred_le := _, min_of_le_pred := _, le_pred_of_lt := _, le_of_pred_lt := _}

@[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 a → pred 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

succ_order.of_succ_le_iff succ hsucc_le_iff = {succ := succ, le_succ := _, max_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}

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

pred_order.of_le_pred_iff pred hle_pred_iff = {pred := pred, pred_le := _, min_of_le_pred := _, le_pred_of_lt := _, le_of_pred_lt := _}

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

order.succ = succ_order.succ

theorem order.le_succ {α : Type u_1} [preorder α] [succ_order α] (a : α) :

a ≤ order.succ a

theorem order.max_of_succ_le {α : Type u_1} [preorder α] [succ_order α] {a : α} :

order.succ a ≤ a → is_max a

theorem order.succ_le_of_lt {α : Type u_1} [preorder α] [succ_order α] {a b : α} :

a < b → order.succ a ≤ b

theorem order.le_of_lt_succ {α : Type u_1} [preorder α] [succ_order α] {a b : α} :

a < order.succ b → a ≤ b

@[simp]

theorem order.succ_le_iff_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} :

order.succ a ≤ a ↔ is_max a

@[simp]

theorem order.lt_succ_iff_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} :

a < order.succ a ↔ ¬is_max a

theorem order.lt_succ_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} :

¬is_max a → a < order.succ 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 ⩿ order.succ a

theorem order.covby_succ_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} (h : ¬is_max a) :

a ⋖ order.succ a

theorem order.lt_succ_iff_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬is_max a) :

b < order.succ a ↔ b ≤ a

theorem order.succ_le_iff_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬is_max a) :

order.succ a ≤ b ↔ a < b

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

order.succ a < order.succ b ↔ a < 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) :

order.succ a ≤ order.succ b ↔ a ≤ b

@[simp]

theorem order.succ_le_succ {α : Type u_1} [preorder α] [succ_order α] {a b : α} (h : a ≤ b) :

order.succ a ≤ order.succ b

theorem order.succ_mono {α : Type u_1} [preorder α] [succ_order α] :

monotone order.succ

theorem order.le_succ_iterate {α : Type u_1} [preorder α] [succ_order α] (k : ℕ) (x : α) :

x ≤ order.succ ^[k] x

theorem order.is_max_iterate_succ_of_eq_of_lt {α : Type u_1} [preorder α] [succ_order α] {a : α} {n m : ℕ} (h_eq : order.succ ^[n] a = order.succ ^[m] a) (h_lt : n < m) :

is_max (order.succ ^[n] a)

theorem order.is_max_iterate_succ_of_eq_of_ne {α : Type u_1} [preorder α] [succ_order α] {a : α} {n m : ℕ} (h_eq : order.succ ^[n] a = order.succ ^[m] a) (h_ne : n ≠ m) :

is_max (order.succ ^[n] a)

theorem order.Iio_succ_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} (ha : ¬is_max a) :

set.Iio (order.succ a) = set.Iic a

theorem order.Ici_succ_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a : α} (ha : ¬is_max a) :

set.Ici (order.succ a) = set.Ioi a

theorem order.Ico_succ_right_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (hb : ¬is_max b) :

set.Ico a (order.succ b) = set.Icc a b

theorem order.Ioo_succ_right_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (hb : ¬is_max b) :

set.Ioo a (order.succ b) = set.Ioc a b

theorem order.Icc_succ_left_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬is_max a) :

set.Icc (order.succ a) b = set.Ioc a b

theorem order.Ico_succ_left_of_not_is_max {α : Type u_1} [preorder α] [succ_order α] {a b : α} (ha : ¬is_max a) :

set.Ico (order.succ a) b = set.Ioo a b

theorem order.lt_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a : α) :

a < order.succ a

@[simp]

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

a < order.succ b ↔ a ≤ b

@[simp]

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

order.succ a ≤ b ↔ a < b

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

order.succ a ≤ order.succ b ↔ a ≤ b

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

order.succ a < order.succ b ↔ a < b

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

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

strict_mono order.succ

theorem order.covby_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a : α) :

a ⋖ order.succ a

@[simp]

theorem order.Iio_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a : α) :

set.Iio (order.succ a) = set.Iic a

@[simp]

theorem order.Ici_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a : α) :

set.Ici (order.succ a) = set.Ioi a

@[simp]

theorem order.Ico_succ_right {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a b : α) :

set.Ico a (order.succ b) = set.Icc a b

@[simp]

theorem order.Ioo_succ_right {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a b : α) :

set.Ioo a (order.succ b) = set.Ioc a b

@[simp]

theorem order.Icc_succ_left {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a b : α) :

set.Icc (order.succ a) b = set.Ioc a b

@[simp]

theorem order.Ico_succ_left {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a b : α) :

set.Ico (order.succ a) b = set.Ioo a b

@[simp]

theorem order.succ_eq_iff_is_max {α : Type u_1} [partial_order α] [succ_order α] {a : α} :

order.succ a = a ↔ is_max a

theorem is_max.succ_eq {α : Type u_1} [partial_order α] [succ_order α] {a : α} :

is_max a → order.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) :

order.succ a = order.succ b ↔ a = b

theorem order.le_le_succ_iff {α : Type u_1} [partial_order α] [succ_order α] {a b : α} :

a ≤ b ∧ b ≤ order.succ a ↔ b = a ∨ b = order.succ a

theorem covby.succ_eq {α : Type u_1} [partial_order α] [succ_order α] {a b : α} (h : a ⋖ b) :

order.succ a = b

theorem wcovby.le_succ {α : Type u_1} [partial_order α] [succ_order α] {a b : α} (h : a ⩿ b) :

b ≤ order.succ a

theorem order.le_succ_iff_eq_or_le {α : Type u_1} [partial_order α] [succ_order α] {a b : α} :

a ≤ order.succ b ↔ a = order.succ b ∨ 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 : α) :

set.Iic (order.succ a) = has_insert.insert (order.succ a) (set.Iic a)

theorem order.Icc_succ_right {α : Type u_1} [partial_order α] [succ_order α] {a b : α} (h : a ≤ order.succ b) :

set.Icc a (order.succ b) = has_insert.insert (order.succ b) (set.Icc a b)

theorem order.Ioc_succ_right {α : Type u_1} [partial_order α] [succ_order α] {a b : α} (h : a < order.succ b) :

set.Ioc a (order.succ b) = has_insert.insert (order.succ b) (set.Ioc a b)

theorem order.Iio_succ_eq_insert_of_not_is_max {α : Type u_1} [partial_order α] [succ_order α] {a : α} (h : ¬is_max a) :

set.Iio (order.succ a) = has_insert.insert a (set.Iio a)

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

set.Ico a (order.succ b) = has_insert.insert b (set.Ico a 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) :

set.Ioo a (order.succ b) = has_insert.insert b (set.Ioo a b)

@[simp]

theorem order.succ_eq_succ_iff {α : Type u_1} [partial_order α] [succ_order α] {a b : α} [no_max_order α] :

order.succ a = order.succ b ↔ a = b

theorem order.succ_injective {α : Type u_1} [partial_order α] [succ_order α] [no_max_order α] :

function.injective order.succ

theorem order.succ_ne_succ_iff {α : Type u_1} [partial_order α] [succ_order α] {a b : α} [no_max_order α] :

order.succ a ≠ order.succ b ↔ a ≠ b

theorem order.succ_ne_succ {α : Type u_1} [partial_order α] [succ_order α] {a b : α} [no_max_order α] :

a ≠ b → order.succ a ≠ order.succ b

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 α] :

order.succ a = b ↔ a ⋖ b

theorem order.Iio_succ_eq_insert {α : Type u_1} [partial_order α] [succ_order α] [no_max_order α] (a : α) :

set.Iio (order.succ a) = has_insert.insert a (set.Iio a)

theorem order.Ico_succ_right_eq_insert {α : Type u_1} [partial_order α] [succ_order α] {a b : α} [no_max_order α] (h : a ≤ b) :

set.Ico a (order.succ b) = has_insert.insert b (set.Ico a b)

theorem order.Ioo_succ_right_eq_insert {α : Type u_1} [partial_order α] [succ_order α] {a b : α} [no_max_order α] (h : a < b) :

set.Ioo a (order.succ b) = has_insert.insert b (set.Ioo a b)

@[simp]

theorem order.succ_top {α : Type u_1} [partial_order α] [succ_order α] [order_top α] :

order.succ ⊤ = ⊤

@[simp]

theorem order.succ_le_iff_eq_top {α : Type u_1} [partial_order α] [succ_order α] {a : α} [order_top α] :

order.succ a ≤ a ↔ a = ⊤

@[simp]

theorem order.lt_succ_iff_ne_top {α : Type u_1} [partial_order α] [succ_order α] {a : α} [order_top α] :

a < order.succ a ↔ a ≠ ⊤

@[simp]

theorem order.lt_succ_bot_iff {α : Type u_1} [partial_order α] [succ_order α] {a : α} [order_bot α] [no_max_order α] :

a < order.succ ⊥ ↔ a = ⊥

theorem order.le_succ_bot_iff {α : Type u_1} [partial_order α] [succ_order α] {a : α} [order_bot α] :

a ≤ order.succ ⊥ ↔ a = ⊥ ∨ a = order.succ ⊥

theorem order.bot_lt_succ {α : Type u_1} [partial_order α] [succ_order α] [order_bot α] [nontrivial α] (a : α) :

⊥ < order.succ a

theorem order.succ_ne_bot {α : Type u_1} [partial_order α] [succ_order α] [order_bot α] [nontrivial α] (a : α) :

order.succ a ≠ ⊥

@[protected, instance]

def order.succ_order.subsingleton {α : Type u_1} [partial_order α] :

subsingleton (succ_order α)

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

order.pred = pred_order.pred

theorem order.pred_le {α : Type u_1} [preorder α] [pred_order α] (a : α) :

order.pred a ≤ a

theorem order.min_of_le_pred {α : Type u_1} [preorder α] [pred_order α] {a : α} :

a ≤ order.pred a → is_min a

theorem order.le_pred_of_lt {α : Type u_1} [preorder α] [pred_order α] {a b : α} :

a < b → a ≤ order.pred b

theorem order.le_of_pred_lt {α : Type u_1} [preorder α] [pred_order α] {a b : α} :

order.pred a < b → a ≤ b

@[simp]

theorem order.le_pred_iff_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} :

a ≤ order.pred a ↔ is_min a

@[simp]

theorem order.pred_lt_iff_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} :

order.pred a < a ↔ ¬is_min a

theorem order.pred_lt_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} :

¬is_min a → order.pred 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 : α) :

order.pred a ⩿ a

theorem order.pred_covby_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} (h : ¬is_min a) :

order.pred a ⋖ a

theorem order.pred_lt_iff_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬is_min a) :

order.pred a < b ↔ a ≤ b

theorem order.le_pred_iff_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬is_min a) :

b ≤ order.pred a ↔ b < a

@[simp]

theorem order.pred_le_pred {α : Type u_1} [preorder α] [pred_order α] {a b : α} (h : a ≤ b) :

order.pred a ≤ order.pred b

theorem order.pred_mono {α : Type u_1} [preorder α] [pred_order α] :

monotone order.pred

theorem order.pred_iterate_le {α : Type u_1} [preorder α] [pred_order α] (k : ℕ) (x : α) :

order.pred ^[k] x ≤ x

theorem order.is_min_iterate_pred_of_eq_of_lt {α : Type u_1} [preorder α] [pred_order α] {a : α} {n m : ℕ} (h_eq : order.pred ^[n] a = order.pred ^[m] a) (h_lt : n < m) :

is_min (order.pred ^[n] a)

theorem order.is_min_iterate_pred_of_eq_of_ne {α : Type u_1} [preorder α] [pred_order α] {a : α} {n m : ℕ} (h_eq : order.pred ^[n] a = order.pred ^[m] a) (h_ne : n ≠ m) :

is_min (order.pred ^[n] a)

theorem order.Ioi_pred_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} (ha : ¬is_min a) :

set.Ioi (order.pred a) = set.Ici a

theorem order.Iic_pred_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a : α} (ha : ¬is_min a) :

set.Iic (order.pred a) = set.Iio a

theorem order.Ioc_pred_left_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬is_min a) :

set.Ioc (order.pred a) b = set.Icc a b

theorem order.Ioo_pred_left_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬is_min a) :

set.Ioo (order.pred a) b = set.Ico a b

theorem order.Icc_pred_right_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬is_min b) :

set.Icc a (order.pred b) = set.Ico a b

theorem order.Ioc_pred_right_of_not_is_min {α : Type u_1} [preorder α] [pred_order α] {a b : α} (ha : ¬is_min b) :

set.Ioc a (order.pred b) = set.Ioo a b

theorem order.pred_lt {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a : α) :

order.pred a < a

@[simp]

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

order.pred a < b ↔ a ≤ b

@[simp]

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

a ≤ order.pred b ↔ a < b

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

order.pred a ≤ order.pred b ↔ a ≤ b

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

order.pred a < order.pred b ↔ a < b

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

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

strict_mono order.pred

theorem order.pred_covby {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a : α) :

order.pred a ⋖ a

@[simp]

theorem order.Ioi_pred {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a : α) :

set.Ioi (order.pred a) = set.Ici a

@[simp]

theorem order.Iic_pred {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a : α) :

set.Iic (order.pred a) = set.Iio a

@[simp]

theorem order.Ioc_pred_left {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a b : α) :

set.Ioc (order.pred a) b = set.Icc a b

@[simp]

theorem order.Ioo_pred_left {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a b : α) :

set.Ioo (order.pred a) b = set.Ico a b

@[simp]

theorem order.Icc_pred_right {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a b : α) :

set.Icc a (order.pred b) = set.Ico a b

@[simp]

theorem order.Ioc_pred_right {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a b : α) :

set.Ioc a (order.pred b) = set.Ioo a b

@[simp]

theorem order.pred_eq_iff_is_min {α : Type u_1} [partial_order α] [pred_order α] {a : α} :

order.pred a = a ↔ is_min a

theorem is_min.pred_eq {α : Type u_1} [partial_order α] [pred_order α] {a : α} :

is_min a → order.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 : α} :

order.pred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = order.pred a

theorem covby.pred_eq {α : Type u_1} [partial_order α] [pred_order α] {a b : α} (h : a ⋖ b) :

order.pred b = a

theorem wcovby.pred_le {α : Type u_1} [partial_order α] [pred_order α] {a b : α} (h : a ⩿ b) :

order.pred b ≤ a

theorem order.pred_le_iff_eq_or_le {α : Type u_1} [partial_order α] [pred_order α] {a b : α} :

order.pred a ≤ b ↔ b = order.pred a ∨ 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 : α) :

set.Ici (order.pred a) = has_insert.insert (order.pred a) (set.Ici a)

theorem order.Ioi_pred_eq_insert_of_not_is_min {α : Type u_1} [partial_order α] [pred_order α] {a : α} (ha : ¬is_min a) :

set.Ioi (order.pred a) = has_insert.insert a (set.Ioi a)

theorem order.Icc_pred_left {α : Type u_1} [partial_order α] [pred_order α] {a b : α} (h : order.pred a ≤ b) :

set.Icc (order.pred a) b = has_insert.insert (order.pred a) (set.Icc a b)

theorem order.Ico_pred_left {α : Type u_1} [partial_order α] [pred_order α] {a b : α} (h : order.pred a < b) :

set.Ico (order.pred a) b = has_insert.insert (order.pred a) (set.Ico a b)

@[simp]

theorem order.pred_eq_pred_iff {α : Type u_1} [partial_order α] [pred_order α] {a b : α} [no_min_order α] :

order.pred a = order.pred b ↔ a = b

theorem order.pred_injective {α : Type u_1} [partial_order α] [pred_order α] [no_min_order α] :

function.injective order.pred

theorem order.pred_ne_pred_iff {α : Type u_1} [partial_order α] [pred_order α] {a b : α} [no_min_order α] :

order.pred a ≠ order.pred b ↔ a ≠ b

theorem order.pred_ne_pred {α : Type u_1} [partial_order α] [pred_order α] {a b : α} [no_min_order α] :

a ≠ b → order.pred a ≠ order.pred b

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 α] :

order.pred b = a ↔ a ⋖ b

theorem order.Ioi_pred_eq_insert {α : Type u_1} [partial_order α] [pred_order α] [no_min_order α] (a : α) :

set.Ioi (order.pred a) = has_insert.insert a (set.Ioi a)

theorem order.Ico_pred_right_eq_insert {α : Type u_1} [partial_order α] [pred_order α] {a b : α} [no_min_order α] (h : a ≤ b) :

set.Ioc (order.pred a) b = has_insert.insert a (set.Ioc a b)

theorem order.Ioo_pred_right_eq_insert {α : Type u_1} [partial_order α] [pred_order α] {a b : α} [no_min_order α] (h : a < b) :

set.Ioo (order.pred a) b = has_insert.insert a (set.Ioo a b)

@[simp]

theorem order.pred_bot {α : Type u_1} [partial_order α] [pred_order α] [order_bot α] :

order.pred ⊥ = ⊥

@[simp]

theorem order.le_pred_iff_eq_bot {α : Type u_1} [partial_order α] [pred_order α] {a : α} [order_bot α] :

a ≤ order.pred a ↔ a = ⊥

@[simp]

theorem order.pred_lt_iff_ne_bot {α : Type u_1} [partial_order α] [pred_order α] {a : α} [order_bot α] :

order.pred a < a ↔ a ≠ ⊥

@[simp]

theorem order.pred_top_lt_iff {α : Type u_1} [partial_order α] [pred_order α] {a : α} [order_top α] [no_min_order α] :

order.pred ⊤ < a ↔ a = ⊤

theorem order.pred_top_le_iff {α : Type u_1} [partial_order α] [pred_order α] {a : α} [order_top α] :

order.pred ⊤ ≤ a ↔ a = ⊤ ∨ a = order.pred ⊤

theorem order.pred_lt_top {α : Type u_1} [partial_order α] [pred_order α] [order_top α] [nontrivial α] (a : α) :

order.pred a < ⊤

theorem order.pred_ne_top {α : Type u_1} [partial_order α] [pred_order α] [order_top α] [nontrivial α] (a : α) :

order.pred a ≠ ⊤

@[protected, instance]

def order.pred_order.subsingleton {α : Type u_1} [partial_order α] :

subsingleton (pred_order α)

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

order.succ (order.pred a) = a

@[simp]

theorem order.pred_succ_of_not_is_max {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] {a : α} (h : ¬is_max a) :

order.pred (order.succ a) = a

@[simp]

theorem order.succ_pred {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] [no_min_order α] (a : α) :

order.succ (order.pred a) = a

@[simp]

theorem order.pred_succ {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] [no_max_order α] (a : α) :

order.pred (order.succ a) = a

theorem order.pred_succ_iterate_of_not_is_max {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] (i : α) (n : ℕ) (hin : ¬is_max (order.succ ^[n - 1] i)) :

order.pred ^[n] (order.succ ^[n] i) = i

theorem order.succ_pred_iterate_of_not_is_min {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] (i : α) (n : ℕ) (hin : ¬is_min (order.pred ^[n - 1] i)) :

order.succ ^[n] (order.pred ^[n] 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 α] [partial_order α] [order_top α] [succ_order α] :

succ_order (with_top α)

Equations

with_top.succ_order = {succ := λ (a : with_top α), with_top.succ_order._match_1 a, le_succ := _, max_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}
with_top.succ_order._match_1 (option.some a) = ite (a = ⊤) ⊤ (option.some (order.succ a))
with_top.succ_order._match_1 ⊤ = ⊤

@[simp]

theorem with_top.succ_coe_top {α : Type u_1} [decidable_eq α] [partial_order α] [order_top α] [succ_order α] :

order.succ ↑⊤ = ⊤

theorem with_top.succ_coe_of_ne_top {α : Type u_1} [decidable_eq α] [partial_order α] [order_top α] [succ_order α] {a : α} (h : a ≠ ⊤) :

order.succ ↑a = ↑(order.succ a)

@[protected, instance]

def with_top.pred_order {α : Type u_1} [preorder α] [order_top α] [pred_order α] :

pred_order (with_top α)

Equations

with_top.pred_order = {pred := λ (a : with_top α), with_top.pred_order._match_1 a, pred_le := _, min_of_le_pred := _, le_pred_of_lt := _, le_of_pred_lt := _}
with_top.pred_order._match_1 (option.some a) = option.some (order.pred a)
with_top.pred_order._match_1 ⊤ = option.some ⊤

@[simp]

theorem with_top.pred_top {α : Type u_1} [preorder α] [order_top α] [pred_order α] :

order.pred ⊤ = ↑⊤

@[simp]

theorem with_top.pred_coe {α : Type u_1} [preorder α] [order_top α] [pred_order α] (a : α) :

order.pred ↑a = ↑(order.pred a)

@[simp]

theorem with_top.pred_untop {α : Type u_1} [preorder α] [order_top α] [pred_order α] (a : with_top α) (ha : a ≠ ⊤) :

order.pred (a.untop ha) = (order.pred a).untop _

Adding a `⊤` to a `no_max_order` #

@[protected, instance]

def with_top.succ_order_of_no_max_order {α : Type u_1} [preorder α] [no_max_order α] [succ_order α] :

succ_order (with_top α)

Equations

with_top.succ_order_of_no_max_order = {succ := λ (a : with_top α), with_top.succ_order_of_no_max_order._match_1 a, le_succ := _, max_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}
with_top.succ_order_of_no_max_order._match_1 (option.some a) = option.some (order.succ a)
with_top.succ_order_of_no_max_order._match_1 ⊤ = ⊤

@[simp]

theorem with_top.succ_coe {α : Type u_1} [preorder α] [no_max_order α] [succ_order α] (a : α) :

order.succ ↑a = ↑(order.succ a)

@[protected, instance]

def with_top.pred_order.is_empty {α : Type u_1} [preorder α] [no_max_order α] [hα : nonempty α] :

is_empty (pred_order (with_top α))

Adding a `⊥` to an `order_bot` #

@[protected, instance]

def with_bot.succ_order {α : Type u_1} [preorder α] [order_bot α] [succ_order α] :

succ_order (with_bot α)

Equations

with_bot.succ_order = {succ := λ (a : with_bot α), with_bot.succ_order._match_1 a, le_succ := _, max_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}
with_bot.succ_order._match_1 (option.some a) = option.some (order.succ a)
with_bot.succ_order._match_1 ⊥ = option.some ⊥

@[simp]

theorem with_bot.succ_bot {α : Type u_1} [preorder α] [order_bot α] [succ_order α] :

order.succ ⊥ = ↑⊥

@[simp]

theorem with_bot.succ_coe {α : Type u_1} [preorder α] [order_bot α] [succ_order α] (a : α) :

order.succ ↑a = ↑(order.succ a)

@[simp]

theorem with_bot.succ_unbot {α : Type u_1} [preorder α] [order_bot α] [succ_order α] (a : with_bot α) (ha : a ≠ ⊥) :

order.succ (a.unbot ha) = (order.succ a).unbot _

@[protected, instance]

def with_bot.pred_order {α : Type u_1} [decidable_eq α] [partial_order α] [order_bot α] [pred_order α] :

pred_order (with_bot α)

Equations

with_bot.pred_order = {pred := λ (a : with_bot α), with_bot.pred_order._match_1 a, pred_le := _, min_of_le_pred := _, le_pred_of_lt := _, le_of_pred_lt := _}
with_bot.pred_order._match_1 (option.some a) = ite (a = ⊥) ⊥ (option.some (order.pred a))
with_bot.pred_order._match_1 ⊥ = ⊥

@[simp]

theorem with_bot.pred_coe_bot {α : Type u_1} [decidable_eq α] [partial_order α] [order_bot α] [pred_order α] :

order.pred ↑⊥ = ⊥

theorem with_bot.pred_coe_of_ne_bot {α : Type u_1} [decidable_eq α] [partial_order α] [order_bot α] [pred_order α] {a : α} (h : a ≠ ⊥) :

order.pred ↑a = ↑(order.pred 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 α] :

is_empty (succ_order (with_bot α))

@[protected, instance]

def with_bot.pred_order_of_no_min_order {α : Type u_1} [preorder α] [no_min_order α] [pred_order α] :

pred_order (with_bot α)

Equations

with_bot.pred_order_of_no_min_order = {pred := λ (a : with_bot α), with_bot.pred_order_of_no_min_order._match_1 a, pred_le := _, min_of_le_pred := _, le_pred_of_lt := _, le_of_pred_lt := _}
with_bot.pred_order_of_no_min_order._match_1 (option.some a) = option.some (order.pred a)
with_bot.pred_order_of_no_min_order._match_1 ⊥ = ⊥

@[simp]

theorem with_bot.pred_coe {α : Type u_1} [preorder α] [no_min_order α] [pred_order α] (a : α) :

order.pred ↑a = ↑(order.pred a)

Archimedeanness #

@[class]

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

Prop

exists_succ_iterate_of_le : ∀ {a b : α}, a ≤ b → (∃ (n : ℕ), order.succ ^[n] a = b)

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

exists_pred_iterate_of_le : ∀ {a b : α}, a ≤ b → (∃ (n : ℕ), order.pred ^[n] b = a)

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

Instances of this typeclass

@[protected, instance]

def order_dual.is_pred_archimedean {α : Type u_1} [preorder α] [succ_order α] [is_succ_archimedean α] :

is_pred_archimedean αᵒᵈ

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 ≤ 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 α] [is_succ_archimedean α] {p : α → Prop} (hsucc : ∀ (a : α), p a ↔ p (order.succ a)) {a b : α} (h : a ≤ b) :

p a ↔ p b

@[protected, instance]

def order_dual.is_succ_archimedean {α : Type u_1} [preorder α] [pred_order α] [is_pred_archimedean α] :

is_succ_archimedean αᵒᵈ

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 ≤ 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 α] [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]

def is_well_order.to_is_pred_archimedean {α : Type u_1} [linear_order α] [h : is_well_order α has_lt.lt] [pred_order α] :

is_pred_archimedean α

@[protected, instance]

def is_well_order.to_is_succ_archimedean {α : Type u_1} [linear_order α] [h : is_well_order α gt] [succ_order α] :

is_succ_archimedean α

theorem succ.rec_bot {α : Type u_1} [preorder α] [order_bot α] [succ_order α] [is_succ_archimedean α] (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 α] [is_pred_archimedean α] (p : α → Prop) (htop : p ⊤) (hpred : ∀ (a : α), p a → p (order.pred a)) (a : α) :

p a