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 #

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

Successor order #

@[ext, class]

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

Type u_2

succ : α → α
le_succ : ∀ (a : α), a ≤ succ_order.succ a
maximal_of_succ_le : ∀ ⦃a : α⦄, succ_order.succ a ≤ a → ∀ ⦃b : α⦄, ¬a < b
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

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

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 := _, maximal_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}

@[simp]

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

succ_order.succ a ≤ succ_order.succ b

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

monotone succ_order.succ

theorem succ_order.lt_succ_of_not_maximal {α : Type u_1} [preorder α] [succ_order α] {a b : α} (h : a < b) :

a < succ_order.succ a

theorem has_lt.lt.lt_succ {α : Type u_1} [preorder α] [succ_order α] {a b : α} (h : a < b) :

a < succ_order.succ a

Alias of lt_succ_of_not_maximal.

@[protected]

theorem has_lt.lt.covby_succ {α : Type u_1} [preorder α] [succ_order α] {a b : α} (h : a < b) :

a ⋖ succ_order.succ a

@[simp]

theorem succ_order.covby_succ_of_nonempty_Ioi {α : Type u_1} [preorder α] [succ_order α] {a : α} (h : (set.Ioi a).nonempty) :

a ⋖ succ_order.succ a

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

a < succ_order.succ a

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

a < succ_order.succ b ↔ a ≤ b

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

succ_order.succ a ≤ b ↔ a < b

@[simp]

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

succ_order.succ a ≤ succ_order.succ b ↔ a ≤ b

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

succ_order.succ a ≤ succ_order.succ b → a ≤ b

Alias of succ_le_succ_iff.

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

succ_order.succ a < succ_order.succ b ↔ a < b

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

a < b → succ_order.succ a < succ_order.succ b

Alias of succ_lt_succ_iff.

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

succ_order.succ a < succ_order.succ b → a < b

Alias of succ_lt_succ_iff.

theorem succ_order.succ_strict_mono {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] :

strict_mono succ_order.succ

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

a ⋖ succ_order.succ a

@[protected, instance]

def 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 succ_order.le_le_succ_iff {α : Type u_1} [partial_order α] [succ_order α] {a b : α} :

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

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

succ_order.succ a = b

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

function.injective succ_order.succ

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

succ_order.succ a = succ_order.succ b ↔ a = b

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

succ_order.succ a ≠ succ_order.succ b ↔ a ≠ b

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

a ≠ b → succ_order.succ a ≠ succ_order.succ b

Alias of succ_ne_succ_iff.

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

succ_order.succ a ≠ succ_order.succ b → 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_max_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_max_order α] {a b : α} :

a ≤ succ_order.succ b ↔ a ≤ b ∨ a = succ_order.succ b

theorem covby_iff_succ_eq {α : Type u_1} [partial_order α] [succ_order α] [no_max_order α] {a b : α} :

a ⋖ b ↔ succ_order.succ a = b

@[simp]

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

succ_order.succ ⊤ = ⊤

@[simp]

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

succ_order.succ a ≤ a ↔ a = ⊤

@[simp]

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

a < succ_order.succ a ↔ a ≠ ⊤

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

⊥ < succ_order.succ a

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

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

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

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

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
minimal_of_le_pred : ∀ ⦃a : α⦄, a ≤ pred_order.pred a → ∀ ⦃b : α⦄, ¬b < 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

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 < 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 := _, minimal_of_le_pred := _, le_pred_of_lt := _, le_of_pred_lt := _}

@[simp]

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

pred_order.pred a ≤ pred_order.pred b

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

monotone pred_order.pred

theorem pred_order.pred_lt_of_not_minimal {α : Type u_1} [preorder α] [pred_order α] {a b : α} (h : b < a) :

pred_order.pred a < a

theorem has_lt.lt.pred_lt {α : Type u_1} [preorder α] [pred_order α] {a b : α} (h : b < a) :

pred_order.pred a < a

Alias of pred_lt_of_not_minimal.

@[protected]

theorem has_lt.lt.pred_covby {α : Type u_1} [preorder α] [pred_order α] {a b : α} (h : b < a) :

pred_order.pred a ⋖ a

@[simp]

theorem pred_order.pred_covby_of_nonempty_Iio {α : Type u_1} [preorder α] [pred_order α] {a : α} (h : (set.Iio a).nonempty) :

pred_order.pred a ⋖ a

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

pred_order.pred a < a

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

pred_order.pred a < b ↔ a ≤ b

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

a ≤ pred_order.pred b ↔ a < b

@[simp]

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

pred_order.pred a ≤ pred_order.pred b ↔ a ≤ b

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

pred_order.pred a ≤ pred_order.pred b → a ≤ b

Alias of pred_le_pred_iff.

@[simp]

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

pred_order.pred a < pred_order.pred b ↔ a < b

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

a < b → pred_order.pred a < pred_order.pred b

Alias of pred_lt_pred_iff.

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

pred_order.pred a < pred_order.pred b → a < b

Alias of pred_lt_pred_iff.

theorem pred_order.pred_strict_mono {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] :

strict_mono pred_order.pred

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

pred_order.pred a ⋖ a

@[protected, instance]

def 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 pred_order.pred_le_le_iff {α : Type u_1} [partial_order α] [pred_order α] {a b : α} :

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

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

pred_order.pred b = a

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

function.injective pred_order.pred

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

pred_order.pred a = pred_order.pred b ↔ a = b

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

pred_order.pred a ≠ pred_order.pred b ↔ a ≠ b

theorem pred_order.pred_lt_iff_lt_or_eq {α : Type u_1} [partial_order α] [pred_order α] [no_min_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_min_order α] {a b : α} :

pred_order.pred a ≤ b ↔ a ≤ b ∨ pred_order.pred a = b

theorem covby_iff_pred_eq {α : Type u_1} [partial_order α] [pred_order α] [no_min_order α] {a b : α} :

a ⋖ b ↔ pred_order.pred b = a

@[simp]

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

pred_order.pred ⊥ = ⊥

@[simp]

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

a ≤ pred_order.pred a ↔ a = ⊥

@[simp]

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

pred_order.pred a < a ↔ a ≠ ⊥

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

pred_order.pred a < ⊤

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

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

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

theorem pred_order.pred_eq_supr {α : Type u_1} [complete_lattice α] [pred_order α] (a : α) :

pred_order.pred a = ⨆ (b : α) (h : b < a), b

Successor-predecessor orders #

@[protected]

theorem has_lt.lt.succ_pred {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] {a b : α} (h : b < a) :

succ_order.succ (pred_order.pred a) = a

@[protected]

theorem has_lt.lt.pred_succ {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] {a b : α} (h : a < b) :

pred_order.pred (succ_order.succ a) = a

@[simp]

theorem succ_pred_of_nonempty_Iio {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] {a : α} (h : (set.Iio a).nonempty) :

succ_order.succ (pred_order.pred a) = a

@[simp]

theorem pred_succ_of_nonempty_Ioi {α : Type u_1} [partial_order α] [succ_order α] [pred_order α] {a : α} (h : (set.Ioi a).nonempty) :

pred_order.pred (succ_order.succ a) = a

@[simp]

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

succ_order.succ (pred_order.pred a) = a

@[simp]

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

pred_order.pred (succ_order.succ a) = a

Dual order #

@[protected, instance]

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

succ_order (order_dual α)

Equations

order_dual.succ_order = {succ := pred_order.pred _inst_2, le_succ := _, maximal_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}

@[protected, instance]

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

pred_order (order_dual α)

Equations

order_dual.pred_order = {pred := succ_order.succ _inst_2, pred_le := _, minimal_of_le_pred := _, le_pred_of_lt := _, le_of_pred_lt := _}

`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 := _, maximal_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}
with_top.succ_order._match_1 (some a) = ite (a = ⊤) ⊤ (some (succ_order.succ a))
with_top.succ_order._match_1 ⊤ = ⊤

@[protected, instance]

def with_top.pred_order {α : Type u_1} [partial_order α] [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 := _, minimal_of_le_pred := _, le_pred_of_lt := _, le_of_pred_lt := _}
with_top.pred_order._match_1 (some a) = some (pred_order.pred a)
with_top.pred_order._match_1 ⊤ = some ⊤

Adding a `⊤` to a `no_max_order` #

@[protected, instance]

def with_top.succ_order_of_no_max_order {α : Type u_1} [partial_order α] [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 := _, maximal_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}
with_top.succ_order_of_no_max_order._match_1 (some a) = some (succ_order.succ a)
with_top.succ_order_of_no_max_order._match_1 ⊤ = ⊤

@[protected, instance]

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

is_empty (pred_order (with_top α))

Adding a `⊥` to a `bot_order` #

@[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 := _, maximal_of_succ_le := _, succ_le_of_lt := _, le_of_lt_succ := _}
with_bot.succ_order._match_1 (some a) = some (succ_order.succ a)
with_bot.succ_order._match_1 ⊥ = some ⊥

@[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 := _, minimal_of_le_pred := _, le_pred_of_lt := _, le_of_pred_lt := _}
with_bot.pred_order._match_1 (some a) = ite (a = ⊥) ⊥ (some (pred_order.pred a))
with_bot.pred_order._match_1 ⊥ = ⊥

Adding a `⊥` to a `no_min_order` #

@[protected, instance]

def succ_order.is_empty {α : Type u_1} [partial_order α] [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} [partial_order α] [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 := _, minimal_of_le_pred := _, le_pred_of_lt := _, le_of_pred_lt := _}
with_bot.pred_order_of_no_min_order._match_1 (some a) = some (pred_order.pred a)
with_bot.pred_order_of_no_min_order._match_1 ⊥ = ⊥

Archimedeanness #

@[class]

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

Prop

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

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

Instances

@[class]

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

Prop

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

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

Instances

@[protected, instance]

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

is_pred_archimedean (order_dual α)

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} {m : α} (h0 : P m) (h1 : ∀ (n : α), m ≤ n → P n → P (succ_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 (succ_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 (order_dual α)

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} {m : α} (h0 : P m) (h1 : ∀ (n : α), n ≤ m → P n → P (pred_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 (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 a → p (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 a → p (pred_order.pred a)) (a : α) :

p a