Documentation

Mathlib.Order.SuccPred.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 #

SuccOrder: Order equipped with a sensible successor function.
PredOrder: Order equipped with a sensible predecessor function.
IsSuccArchimedean: SuccOrder where succ iterated to an element gives all the greater ones.
IsPredArchimedean: PredOrder 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 NaiveSuccOrder (α : Type _) [Preorder α] :=
(succ : α → α)
(succ_le_iff : ∀ {a b}, succ a ≤ b ↔ a < b)
(lt_succ_iff : ∀ {a b}, a < succ b ↔ a ≤ b)
→ α)
(succ_le_iff : ∀ {a b}, succ a ≤ b ↔ a < b)
(lt_succ_iff : ∀ {a b}, a < succ b ↔ a ≤ b)
∀ {a b}, succ a ≤ b ↔ a < b)
(lt_succ_iff : ∀ {a b}, a < succ b ↔ a ≤ b)
≤ b ↔ a < b)
(lt_succ_iff : ∀ {a b}, a < succ b ↔ a ≤ b)
↔ a < b)
(lt_succ_iff : ∀ {a b}, a < succ b ↔ a ≤ b)
∀ {a b}, a < succ b ↔ a ≤ b)
↔ a ≤ b)
≤ b)

can't apply to an OrderTop 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 SuccOrder α and NoMaxOrder α.

TODO #

Is GaloisConnection pred succ always true? If not, we should introduce

class SuccPredOrder (α : Type _) [Preorder α] extends SuccOrder α, PredOrder α :=
(pred_succ_gc : GaloisConnection (pred : α → α) succ)
→ α) succ)

covby should help here.

theorem SuccOrder.ext_iff {α : Type u_1} :

∀ {inst : Preorder α} (x y : SuccOrder α), x = y ↔ SuccOrder.succ = SuccOrder.succ

theorem SuccOrder.ext {α : Type u_1} :

∀ {inst : Preorder α} (x y : SuccOrder α), SuccOrder.succ = SuccOrder.succ → x = y

class SuccOrder (α : Type u_1) [inst : Preorder α] :

Type u_1

Successor function
succ : α → α
Proof of basic ordering with respect to succ
le_succ : ∀ (a : α), a ≤ succ a
Proof of interaction between succ and maximal element
max_of_succ_le : ∀ {a : α}, succ a ≤ a → IsMax a
Proof that succ satifies ordering invariants betweeen LT and LE
succ_le_of_lt : ∀ {a b : α}, a < b → succ a ≤ b
Proof that succ satifies ordering invariants betweeen LE and LT
le_of_lt_succ : ∀ {a b : α}, a < succ b → a ≤ b

Order equipped with a sensible successor function.

Instances

theorem PredOrder.ext {α : Type u_1} :

∀ {inst : Preorder α} (x y : PredOrder α), PredOrder.pred = PredOrder.pred → x = y

theorem PredOrder.ext_iff {α : Type u_1} :

∀ {inst : Preorder α} (x y : PredOrder α), x = y ↔ PredOrder.pred = PredOrder.pred

class PredOrder (α : Type u_1) [inst : Preorder α] :

Type u_1

Predecessor function
pred : α → α
Proof of basic ordering with respect to pred
pred_le : ∀ (a : α), pred a ≤ a
Proof of interaction between pred and minimal element
min_of_le_pred : ∀ {a : α}, a ≤ pred a → IsMin a
Proof that pred satifies ordering invariants betweeen LT and LE
le_pred_of_lt : ∀ {a b : α}, a < b → a ≤ pred b
Proof that pred satifies ordering invariants betweeen LE and LT
le_of_pred_lt : ∀ {a b : α}, pred a < b → a ≤ b

Order equipped with a sensible predecessor function.

Instances

instance instPredOrderOrderDualPreorder {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] :

PredOrder αᵒᵈ

Equations

One or more equations did not get rendered due to their size.

instance instSuccOrderOrderDualPreorder {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] :

SuccOrder αᵒᵈ

Equations

One or more equations did not get rendered due to their size.

def SuccOrder.ofSuccLeIffOfLeLtSucc {α : Type u_1} [inst : 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 SuccOrder α usable when α has no maximal element.

Equations

One or more equations did not get rendered due to their size.

def PredOrder.ofLePredIffOfPredLePred {α : Type u_1} [inst : 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 PredOrder α usable when α has no minimal element.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem SuccOrder.ofCore_succ {α : Type u_1} [inst : LinearOrder α] (succ : α → α) (hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b) (hm : ∀ (a : α), IsMax a → succ a = a) :

∀ (a : α), SuccOrder.succ a = succ a

def SuccOrder.ofCore {α : Type u_1} [inst : LinearOrder α] (succ : α → α) (hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b) (hm : ∀ (a : α), IsMax a → succ a = a) :

A constructor for SuccOrder α for α a linear order.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem PredOrder.ofCore_pred {α : Type u_1} [inst : LinearOrder α] (pred : α → α) (hn : ∀ {a : α}, ¬IsMin a → ∀ (b : α), b ≤ pred a ↔ b < a) (hm : ∀ (a : α), IsMin a → pred a = a) :

∀ (a : α), PredOrder.pred a = pred a

def PredOrder.ofCore {α : Type u_1} [inst : LinearOrder α] (pred : α → α) (hn : ∀ {a : α}, ¬IsMin a → ∀ (b : α), b ≤ pred a ↔ b < a) (hm : ∀ (a : α), IsMin a → pred a = a) :

A constructor for PredOrder α for α a linear order.

Equations

One or more equations did not get rendered due to their size.

def SuccOrder.ofSuccLeIff {α : Type u_1} [inst : LinearOrder α] (succ : α → α) (hsucc_le_iff : ∀ {a b : α}, succ a ≤ b ↔ a < b) :

A constructor for SuccOrder α usable when α is a linear order with no maximal element.

Equations

One or more equations did not get rendered due to their size.

def PredOrder.ofLePredIff {α : Type u_1} [inst : LinearOrder α] (pred : α → α) (hle_pred_iff : ∀ {a b : α}, a ≤ pred b ↔ a < b) :

A constructor for PredOrder α usable when α is a linear order with no minimal element.

Equations

One or more equations did not get rendered due to their size.

Successor order #

def Order.succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] :

α → α

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 = SuccOrder.succ

theorem Order.le_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] (a : α) :

a ≤ Order.succ a

theorem Order.max_of_succ_le {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} :

Order.succ a ≤ a → IsMax a

theorem Order.succ_le_of_lt {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} :

a < b → Order.succ a ≤ b

theorem Order.le_of_lt_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} :

a < Order.succ b → a ≤ b

@[simp]

theorem Order.succ_le_iff_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} :

Order.succ a ≤ a ↔ IsMax a

@[simp]

theorem Order.lt_succ_iff_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} :

a < Order.succ a ↔ ¬IsMax a

theorem Order.lt_succ_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} :

¬IsMax a → a < Order.succ a

Alias of the reverse direction of Order.lt_succ_iff_not_isMax.

theorem Order.wcovby_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] (a : α) :

a ⩿ Order.succ a

theorem Order.covby_succ_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} (h : ¬IsMax a) :

a ⋖ Order.succ a

theorem Order.lt_succ_iff_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) :

b < Order.succ a ↔ b ≤ a

theorem Order.succ_le_iff_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) :

Order.succ a ≤ b ↔ a < b

theorem Order.succ_lt_succ_iff_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) (hb : ¬IsMax b) :

Order.succ a < Order.succ b ↔ a < b

theorem Order.succ_le_succ_iff_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) (hb : ¬IsMax b) :

Order.succ a ≤ Order.succ b ↔ a ≤ b

@[simp]

theorem Order.succ_le_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (h : a ≤ b) :

Order.succ a ≤ Order.succ b

theorem Order.succ_mono {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] :

Monotone Order.succ

theorem Order.le_succ_iterate {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] (k : ℕ) (x : α) :

x ≤ (Order.succ ^[k]) x

theorem Order.isMax_iterate_succ_of_eq_of_lt {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {n : ℕ} {m : ℕ} (h_eq : (Order.succ ^[n]) a = (Order.succ ^[m]) a) (h_lt : n < m) :

IsMax ((Order.succ ^[n]) a)

theorem Order.isMax_iterate_succ_of_eq_of_ne {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {n : ℕ} {m : ℕ} (h_eq : (Order.succ ^[n]) a = (Order.succ ^[m]) a) (h_ne : n ≠ m) :

IsMax ((Order.succ ^[n]) a)

theorem Order.Iio_succ_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} (ha : ¬IsMax a) :

Set.Iio (Order.succ a) = Set.Iic a

theorem Order.Ici_succ_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} (ha : ¬IsMax a) :

Set.Ici (Order.succ a) = Set.Ioi a

theorem Order.Ico_succ_right_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (hb : ¬IsMax b) :

Set.Ico a (Order.succ b) = Set.Icc a b

theorem Order.Ioo_succ_right_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (hb : ¬IsMax b) :

Set.Ioo a (Order.succ b) = Set.Ioc a b

theorem Order.Icc_succ_left_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) :

Set.Icc (Order.succ a) b = Set.Ioc a b

theorem Order.Ico_succ_left_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) :

Set.Ico (Order.succ a) b = Set.Ioo a b

theorem Order.lt_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) :

a < Order.succ a

@[simp]

theorem Order.lt_succ_iff {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

a < Order.succ b ↔ a ≤ b

@[simp]

theorem Order.succ_le_iff {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

Order.succ a ≤ b ↔ a < b

theorem Order.succ_le_succ_iff {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

Order.succ a ≤ Order.succ b ↔ a ≤ b

theorem Order.succ_lt_succ_iff {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

Order.succ a < Order.succ b ↔ a < b

theorem Order.le_of_succ_le_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

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} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

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} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

Order.succ a < Order.succ b → a < b

Alias of the forward direction of Order.succ_lt_succ_iff.

theorem Order.succ_strictMono {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] :

StrictMono Order.succ

theorem Order.covby_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) :

a ⋖ Order.succ a

@[simp]

theorem Order.Iio_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) :

Set.Iio (Order.succ a) = Set.Iic a

@[simp]

theorem Order.Ici_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) :

Set.Ici (Order.succ a) = Set.Ioi a

@[simp]

theorem Order.Ico_succ_right {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) (b : α) :

Set.Ico a (Order.succ b) = Set.Icc a b

@[simp]

theorem Order.Ioo_succ_right {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) (b : α) :

Set.Ioo a (Order.succ b) = Set.Ioc a b

@[simp]

theorem Order.Icc_succ_left {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) (b : α) :

Set.Icc (Order.succ a) b = Set.Ioc a b

@[simp]

theorem Order.Ico_succ_left {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) (b : α) :

Set.Ico (Order.succ a) b = Set.Ioo a b

@[simp]

theorem Order.succ_eq_iff_isMax {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} :

Order.succ a = a ↔ IsMax a

theorem IsMax.succ_eq {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} :

IsMax a → Order.succ a = a

Alias of the reverse direction of Order.succ_eq_iff_isMax.

theorem Order.succ_eq_succ_iff_of_not_isMax {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) (hb : ¬IsMax b) :

Order.succ a = Order.succ b ↔ a = b

theorem Order.le_le_succ_iff {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} :

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

theorem Order.Covby.succ_eq {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} (h : a ⋖ b) :

Order.succ a = b

theorem Order.Wcovby.le_succ {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} (h : a ⩿ b) :

b ≤ Order.succ a

theorem Order.le_succ_iff_eq_or_le {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} :

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

theorem Order.lt_succ_iff_eq_or_lt_of_not_isMax {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} (hb : ¬IsMax b) :

a < Order.succ b ↔ a = b ∨ a < b

theorem Order.Iic_succ {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] (a : α) :

Set.Iic (Order.succ a) = insert (Order.succ a) (Set.Iic a)

theorem Order.Icc_succ_right {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} (h : a ≤ Order.succ b) :

Set.Icc a (Order.succ b) = insert (Order.succ b) (Set.Icc a b)

theorem Order.Ioc_succ_right {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} (h : a < Order.succ b) :

Set.Ioc a (Order.succ b) = insert (Order.succ b) (Set.Ioc a b)

theorem Order.Iio_succ_eq_insert_of_not_isMax {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} (h : ¬IsMax a) :

Set.Iio (Order.succ a) = insert a (Set.Iio a)

theorem Order.Ico_succ_right_eq_insert_of_not_isMax {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} (h₁ : a ≤ b) (h₂ : ¬IsMax b) :

Set.Ico a (Order.succ b) = insert b (Set.Ico a b)

theorem Order.Ioo_succ_right_eq_insert_of_not_isMax {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} (h₁ : a < b) (h₂ : ¬IsMax b) :

Set.Ioo a (Order.succ b) = insert b (Set.Ioo a b)

@[simp]

theorem Order.succ_eq_succ_iff {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

Order.succ a = Order.succ b ↔ a = b

theorem Order.succ_injective {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : NoMaxOrder α] :

Function.Injective Order.succ

theorem Order.succ_ne_succ_iff {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

Order.succ a ≠ Order.succ b ↔ a ≠ b

theorem Order.succ_ne_succ {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

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} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

a < Order.succ b ↔ a = b ∨ a < b

theorem Order.succ_eq_iff_covby {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

Order.succ a = b ↔ a ⋖ b

theorem Order.Iio_succ_eq_insert {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) :

Set.Iio (Order.succ a) = insert a (Set.Iio a)

theorem Order.Ico_succ_right_eq_insert {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] (h : a ≤ b) :

Set.Ico a (Order.succ b) = insert b (Set.Ico a b)

theorem Order.Ioo_succ_right_eq_insert {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] (h : a < b) :

Set.Ioo a (Order.succ b) = insert b (Set.Ioo a b)

@[simp]

theorem Order.succ_top {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : OrderTop α] :

Order.succ ⊤ = ⊤

theorem Order.succ_le_iff_eq_top {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} [inst : OrderTop α] :

Order.succ a ≤ a ↔ a = ⊤

theorem Order.lt_succ_iff_ne_top {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} [inst : OrderTop α] :

a < Order.succ a ↔ a ≠ ⊤

theorem Order.lt_succ_bot_iff {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} [inst : OrderBot α] [inst : NoMaxOrder α] :

a < Order.succ ⊥ ↔ a = ⊥

theorem Order.le_succ_bot_iff {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} [inst : OrderBot α] :

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

theorem Order.bot_lt_succ {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : OrderBot α] [inst : Nontrivial α] (a : α) :

⊥ < Order.succ a

theorem Order.succ_ne_bot {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : OrderBot α] [inst : Nontrivial α] (a : α) :

Order.succ a ≠ ⊥

instance Order.instSubsingletonSuccOrderToPreorder {α : Type u_1} [inst : PartialOrder α] :

Subsingleton (SuccOrder α)

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

Equations

@Order.instSubsingletonSuccOrderToPreorder = @Order.instSubsingletonSuccOrderToPreorder.proof_1

theorem Order.succ_eq_infᵢ {α : Type u_1} [inst : CompleteLattice α] [inst : SuccOrder α] (a : α) :

Order.succ a = ⨅ b, ⨅ _h, b

Predecessor order #

def Order.pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] :

α → α

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 = PredOrder.pred

theorem Order.pred_le {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] (a : α) :

Order.pred a ≤ a

theorem Order.min_of_le_pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} :

a ≤ Order.pred a → IsMin a

theorem Order.le_pred_of_lt {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} :

a < b → a ≤ Order.pred b

theorem Order.le_of_pred_lt {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} :

Order.pred a < b → a ≤ b

@[simp]

theorem Order.le_pred_iff_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} :

a ≤ Order.pred a ↔ IsMin a

@[simp]

theorem Order.pred_lt_iff_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} :

Order.pred a < a ↔ ¬IsMin a

theorem Order.pred_lt_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} :

¬IsMin a → Order.pred a < a

Alias of the reverse direction of Order.pred_lt_iff_not_isMin.

theorem Order.pred_wcovby {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] (a : α) :

Order.pred a ⩿ a

theorem Order.pred_covby_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} (h : ¬IsMin a) :

Order.pred a ⋖ a

theorem Order.pred_lt_iff_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :

Order.pred a < b ↔ a ≤ b

theorem Order.le_pred_iff_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :

b ≤ Order.pred a ↔ b < a

@[simp]

theorem Order.pred_le_pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (h : a ≤ b) :

Order.pred a ≤ Order.pred b

theorem Order.pred_mono {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] :

Monotone Order.pred

theorem Order.pred_iterate_le {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] (k : ℕ) (x : α) :

(Order.pred ^[k]) x ≤ x

theorem Order.isMin_iterate_pred_of_eq_of_lt {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {n : ℕ} {m : ℕ} (h_eq : (Order.pred ^[n]) a = (Order.pred ^[m]) a) (h_lt : n < m) :

IsMin ((Order.pred ^[n]) a)

theorem Order.isMin_iterate_pred_of_eq_of_ne {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {n : ℕ} {m : ℕ} (h_eq : (Order.pred ^[n]) a = (Order.pred ^[m]) a) (h_ne : n ≠ m) :

IsMin ((Order.pred ^[n]) a)

theorem Order.Ioi_pred_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} (ha : ¬IsMin a) :

Set.Ioi (Order.pred a) = Set.Ici a

theorem Order.Iic_pred_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} (ha : ¬IsMin a) :

Set.Iic (Order.pred a) = Set.Iio a

theorem Order.Ioc_pred_left_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :

Set.Ioc (Order.pred a) b = Set.Icc a b

theorem Order.Ioo_pred_left_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :

Set.Ioo (Order.pred a) b = Set.Ico a b

theorem Order.Icc_pred_right_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin b) :

Set.Icc a (Order.pred b) = Set.Ico a b

theorem Order.Ioc_pred_right_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin b) :

Set.Ioc a (Order.pred b) = Set.Ioo a b

theorem Order.pred_lt {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) :

Order.pred a < a

@[simp]

theorem Order.pred_lt_iff {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

Order.pred a < b ↔ a ≤ b

@[simp]

theorem Order.le_pred_iff {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

a ≤ Order.pred b ↔ a < b

theorem Order.pred_le_pred_iff {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

Order.pred a ≤ Order.pred b ↔ a ≤ b

theorem Order.pred_lt_pred_iff {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

Order.pred a < Order.pred b ↔ a < b

theorem Order.le_of_pred_le_pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

Order.pred a ≤ Order.pred b → a ≤ b

Alias of the forward direction of Order.pred_le_pred_iff.

theorem Order.lt_of_pred_lt_pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

Order.pred a < Order.pred b → a < b

Alias of the forward direction of Order.pred_lt_pred_iff.

theorem Order.pred_lt_pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

a < b → Order.pred a < Order.pred b

Alias of the reverse direction of Order.pred_lt_pred_iff.

theorem Order.pred_strictMono {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] :

StrictMono Order.pred

theorem Order.pred_covby {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) :

Order.pred a ⋖ a

@[simp]

theorem Order.Ioi_pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) :

Set.Ioi (Order.pred a) = Set.Ici a

@[simp]

theorem Order.Iic_pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) :

Set.Iic (Order.pred a) = Set.Iio a

@[simp]

theorem Order.Ioc_pred_left {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) (b : α) :

Set.Ioc (Order.pred a) b = Set.Icc a b

@[simp]

theorem Order.Ioo_pred_left {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) (b : α) :

Set.Ioo (Order.pred a) b = Set.Ico a b

@[simp]

theorem Order.Icc_pred_right {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) (b : α) :

Set.Icc a (Order.pred b) = Set.Ico a b

@[simp]

theorem Order.Ioc_pred_right {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) (b : α) :

Set.Ioc a (Order.pred b) = Set.Ioo a b

@[simp]

theorem Order.pred_eq_iff_isMin {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} :

Order.pred a = a ↔ IsMin a

theorem IsMin.pred_eq {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} :

IsMin a → Order.pred a = a

Alias of the reverse direction of Order.pred_eq_iff_isMin.

theorem Order.pred_le_le_iff {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} :

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

theorem Order.Covby.pred_eq {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} (h : a ⋖ b) :

Order.pred b = a

theorem Order.Wcovby.pred_le {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} (h : a ⩿ b) :

Order.pred b ≤ a

theorem Order.pred_le_iff_eq_or_le {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} :

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

theorem Order.pred_lt_iff_eq_or_lt_of_not_isMin {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :

Order.pred a < b ↔ a = b ∨ a < b

theorem Order.Ici_pred {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] (a : α) :

Set.Ici (Order.pred a) = insert (Order.pred a) (Set.Ici a)

theorem Order.Ioi_pred_eq_insert_of_not_isMin {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} (ha : ¬IsMin a) :

Set.Ioi (Order.pred a) = insert a (Set.Ioi a)

theorem Order.Icc_pred_left {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} (h : Order.pred a ≤ b) :

Set.Icc (Order.pred a) b = insert (Order.pred a) (Set.Icc a b)

theorem Order.Ico_pred_left {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} (h : Order.pred a < b) :

Set.Ico (Order.pred a) b = insert (Order.pred a) (Set.Ico a b)

@[simp]

theorem Order.pred_eq_pred_iff {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

Order.pred a = Order.pred b ↔ a = b

theorem Order.pred_injective {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] [inst : NoMinOrder α] :

Function.Injective Order.pred

theorem Order.pred_ne_pred_iff {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

Order.pred a ≠ Order.pred b ↔ a ≠ b

theorem Order.pred_ne_pred {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

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} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

Order.pred a < b ↔ a = b ∨ a < b

theorem Order.pred_eq_iff_covby {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

Order.pred b = a ↔ a ⋖ b

theorem Order.Ioi_pred_eq_insert {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) :

Set.Ioi (Order.pred a) = insert a (Set.Ioi a)

theorem Order.Ico_pred_right_eq_insert {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] (h : a ≤ b) :

Set.Ioc (Order.pred a) b = insert a (Set.Ioc a b)

theorem Order.Ioo_pred_right_eq_insert {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] (h : a < b) :

Set.Ioo (Order.pred a) b = insert a (Set.Ioo a b)

@[simp]

theorem Order.pred_bot {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] [inst : OrderBot α] :

Order.pred ⊥ = ⊥

theorem Order.le_pred_iff_eq_bot {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} [inst : OrderBot α] :

a ≤ Order.pred a ↔ a = ⊥

theorem Order.pred_lt_iff_ne_bot {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} [inst : OrderBot α] :

Order.pred a < a ↔ a ≠ ⊥

theorem Order.pred_top_lt_iff {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} [inst : OrderTop α] [inst : NoMinOrder α] :

Order.pred ⊤ < a ↔ a = ⊤

theorem Order.pred_top_le_iff {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} [inst : OrderTop α] :

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

theorem Order.pred_lt_top {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] [inst : OrderTop α] [inst : Nontrivial α] (a : α) :

Order.pred a < ⊤

theorem Order.pred_ne_top {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] [inst : OrderTop α] [inst : Nontrivial α] (a : α) :

Order.pred a ≠ ⊤

instance Order.instSubsingletonPredOrderToPreorder {α : Type u_1} [inst : PartialOrder α] :

Subsingleton (PredOrder α)

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

Equations

@Order.instSubsingletonPredOrderToPreorder = @Order.instSubsingletonPredOrderToPreorder.proof_1

theorem Order.pred_eq_supᵢ {α : Type u_1} [inst : CompleteLattice α] [inst : PredOrder α] (a : α) :

Order.pred a = ⨆ b, ⨆ _h, b

Successor-predecessor orders #

@[simp]

theorem Order.succ_pred_of_not_isMin {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : PredOrder α] {a : α} (h : ¬IsMin a) :

Order.succ (Order.pred a) = a

@[simp]

theorem Order.pred_succ_of_not_isMax {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : PredOrder α] {a : α} (h : ¬IsMax a) :

Order.pred (Order.succ a) = a

theorem Order.succ_pred {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) :

Order.succ (Order.pred a) = a

theorem Order.pred_succ {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : PredOrder α] [inst : NoMaxOrder α] (a : α) :

Order.pred (Order.succ a) = a

theorem Order.pred_succ_iterate_of_not_isMax {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : PredOrder α] (i : α) (n : ℕ) (hin : ¬IsMax ((Order.succ ^[n - 1]) i)) :

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

theorem Order.succ_pred_iterate_of_not_isMin {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : PredOrder α] (i : α) (n : ℕ) (hin : ¬IsMin ((Order.pred ^[n - 1]) i)) :

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

`WithBot`, `WithTop` #

Adding a greatest/least element to a SuccOrder or to a PredOrder.

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 OrderTop: Preserves succ and pred.
Adding a ⊤⊤ to a NoMaxOrder: Preserves succ. Never preserves pred.
Adding a ⊥⊥ to an OrderBot: Preserves succ and pred.
Adding a ⊥⊥ to a NoMinOrder: Preserves pred. Never preserves succ. where "preserves (succ/pred)" means (Succ/Pred)Order α → (Succ/Pred)Order ((WithTop/WithBot) α)→ (Succ/Pred)Order ((WithTop/WithBot) α).

Adding a `⊤⊤` to an `OrderTop` #

instance WithTop.instSuccOrderWithTopPreorderToPreorder {α : Type u_1} [inst : DecidableEq α] [inst : PartialOrder α] [inst : OrderTop α] [inst : SuccOrder α] :

SuccOrder (WithTop α)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem WithTop.succ_coe_top {α : Type u_1} [inst : DecidableEq α] [inst : PartialOrder α] [inst : OrderTop α] [inst : SuccOrder α] :

Order.succ ↑⊤ = ⊤

theorem WithTop.succ_coe_of_ne_top {α : Type u_1} [inst : DecidableEq α] [inst : PartialOrder α] [inst : OrderTop α] [inst : SuccOrder α] {a : α} (h : a ≠ ⊤) :

Order.succ ↑a = ↑(Order.succ a)

instance WithTop.instPredOrderWithTopPreorder {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] [inst : PredOrder α] :

PredOrder (WithTop α)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem WithTop.pred_top {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] [inst : PredOrder α] :

Order.pred ⊤ = ↑⊤

@[simp]

theorem WithTop.pred_coe {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] [inst : PredOrder α] (a : α) :

Order.pred ↑a = ↑(Order.pred a)

@[simp]

theorem WithTop.pred_untop {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] [inst : PredOrder α] (a : WithTop α) (ha : a ≠ ⊤) :

Order.pred (WithTop.untop a ha) = WithTop.untop (Order.pred a) (_ : Order.pred a ≠ ⊤)

Adding a `⊤⊤` to a `NoMaxOrder` #

instance WithTop.succOrderOfNoMaxOrder {α : Type u_1} [inst : Preorder α] [inst : NoMaxOrder α] [inst : SuccOrder α] :

SuccOrder (WithTop α)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem WithTop.succ_coe {α : Type u_1} [inst : Preorder α] [inst : NoMaxOrder α] [inst : SuccOrder α] (a : α) :

Order.succ ↑a = ↑(Order.succ a)

instance WithTop.instIsEmptyPredOrderWithTopPreorder {α : Type u_1} [inst : Preorder α] [inst : NoMaxOrder α] [hα : Nonempty α] :

IsEmpty (PredOrder (WithTop α))

Equations

@WithTop.instIsEmptyPredOrderWithTopPreorder = @WithTop.instIsEmptyPredOrderWithTopPreorder.proof_1

Adding a `⊥⊥` to an `OrderBot` #

instance WithBot.instSuccOrderWithBotPreorder {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] [inst : SuccOrder α] :

SuccOrder (WithBot α)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem WithBot.succ_bot {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] [inst : SuccOrder α] :

Order.succ ⊥ = ↑⊥

@[simp]

theorem WithBot.succ_coe {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] [inst : SuccOrder α] (a : α) :

Order.succ ↑a = ↑(Order.succ a)

@[simp]

theorem WithBot.succ_unbot {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] [inst : SuccOrder α] (a : WithBot α) (ha : a ≠ ⊥) :

Order.succ (WithBot.unbot a ha) = WithBot.unbot (Order.succ a) (_ : Order.succ a ≠ ⊥)

instance WithBot.instPredOrderWithBotPreorderToPreorder {α : Type u_1} [inst : DecidableEq α] [inst : PartialOrder α] [inst : OrderBot α] [inst : PredOrder α] :

PredOrder (WithBot α)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem WithBot.pred_coe_bot {α : Type u_1} [inst : DecidableEq α] [inst : PartialOrder α] [inst : OrderBot α] [inst : PredOrder α] :

Order.pred ↑⊥ = ⊥

theorem WithBot.pred_coe_of_ne_bot {α : Type u_1} [inst : DecidableEq α] [inst : PartialOrder α] [inst : OrderBot α] [inst : PredOrder α] {a : α} (h : a ≠ ⊥) :

Order.pred ↑a = ↑(Order.pred a)

Adding a `⊥⊥` to a `NoMinOrder` #

instance WithBot.instIsEmptySuccOrderWithBotPreorder {α : Type u_1} [inst : Preorder α] [inst : NoMinOrder α] [hα : Nonempty α] :

IsEmpty (SuccOrder (WithBot α))

Equations

@WithBot.instIsEmptySuccOrderWithBotPreorder = @WithBot.instIsEmptySuccOrderWithBotPreorder.proof_1

instance WithBot.predOrderOfNoMinOrder {α : Type u_1} [inst : Preorder α] [inst : NoMinOrder α] [inst : PredOrder α] :

PredOrder (WithBot α)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem WithBot.pred_coe {α : Type u_1} [inst : Preorder α] [inst : NoMinOrder α] [inst : PredOrder α] (a : α) :

Order.pred ↑a = ↑(Order.pred a)

Archimedeanness #

class IsSuccArchimedean (α : Type u_1) [inst : Preorder α] [inst : SuccOrder α] :

If a ≤ b≤ b then one can get to a from b by iterating succ
exists_succ_iterate_of_le : ∀ {a b : α}, a ≤ b → ∃ n, (Order.succ ^[n]) a = b

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

Instances

class IsPredArchimedean (α : Type u_1) [inst : Preorder α] [inst : PredOrder α] :

If a ≤ b≤ b then one can get to b from a by iterating pred
exists_pred_iterate_of_le : ∀ {a b : α}, a ≤ b → ∃ n, (Order.pred ^[n]) b = a

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

Instances

instance instIsPredArchimedeanOrderDualPreorderInstPredOrderOrderDualPreorder {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : IsSuccArchimedean α] :

IsPredArchimedean αᵒᵈ

Equations

@instIsPredArchimedeanOrderDualPreorderInstPredOrderOrderDualPreorder = @instIsPredArchimedeanOrderDualPreorderInstPredOrderOrderDualPreorder.proof_1

theorem LE.le.exists_succ_iterate {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : IsSuccArchimedean α] {a : α} {b : α} (h : a ≤ b) :

∃ n, (Order.succ ^[n]) a = b

theorem exists_succ_iterate_iff_le {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : IsSuccArchimedean α] {a : α} {b : α} :

(∃ n, (Order.succ ^[n]) a = b) ↔ a ≤ b

theorem Succ.rec {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : IsSuccArchimedean α] {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 SuccOrder for all elements above a given element m.

theorem Succ.rec_iff {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : IsSuccArchimedean α] {p : α → Prop} (hsucc : ∀ (a : α), p a ↔ p (Order.succ a)) {a : α} {b : α} (h : a ≤ b) :

p a ↔ p b

instance instIsSuccArchimedeanOrderDualPreorderInstSuccOrderOrderDualPreorder {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : IsPredArchimedean α] :

IsSuccArchimedean αᵒᵈ

Equations

@instIsSuccArchimedeanOrderDualPreorderInstSuccOrderOrderDualPreorder = @instIsSuccArchimedeanOrderDualPreorderInstSuccOrderOrderDualPreorder.proof_1

theorem LE.le.exists_pred_iterate {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : IsPredArchimedean α] {a : α} {b : α} (h : a ≤ b) :

∃ n, (Order.pred ^[n]) b = a

theorem exists_pred_iterate_iff_le {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : IsPredArchimedean α] {a : α} {b : α} :

(∃ n, (Order.pred ^[n]) b = a) ↔ a ≤ b

theorem Pred.rec {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : IsPredArchimedean α] {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 PredOrder for all elements below a given element m.

theorem Pred.rec_iff {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : IsPredArchimedean α] {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} [inst : LinearOrder α] [inst : SuccOrder α] [inst : IsSuccArchimedean α] {a : α} {b : α} :

(∃ n, (Order.succ ^[n]) a = b) ∨ ∃ n, (Order.succ ^[n]) b = a

theorem Succ.rec_linear {α : Type u_1} [inst : LinearOrder α] [inst : SuccOrder α] [inst : IsSuccArchimedean α] {p : α → Prop} (hsucc : ∀ (a : α), p a ↔ p (Order.succ a)) (a : α) (b : α) :

p a ↔ p b

theorem exists_pred_iterate_or {α : Type u_1} [inst : LinearOrder α] [inst : PredOrder α] [inst : IsPredArchimedean α] {a : α} {b : α} :

(∃ n, (Order.pred ^[n]) b = a) ∨ ∃ n, (Order.pred ^[n]) a = b

theorem Pred.rec_linear {α : Type u_1} [inst : LinearOrder α] [inst : PredOrder α] [inst : IsPredArchimedean α] {p : α → Prop} (hsucc : ∀ (a : α), p a ↔ p (Order.pred a)) (a : α) (b : α) :

p a ↔ p b

instance IsWellOrder.toIsPredArchimedean {α : Type u_1} [inst : LinearOrder α] [h : IsWellOrder α fun x x_1 => x < x_1] [inst : PredOrder α] :

IsPredArchimedean α

Equations

@IsWellOrder.toIsPredArchimedean = @IsWellOrder.toIsPredArchimedean.proof_1

instance IsWellOrder.toIsSuccArchimedean {α : Type u_1} [inst : LinearOrder α] [h : IsWellOrder α fun x x_1 => x > x_1] [inst : SuccOrder α] :

IsSuccArchimedean α

Equations

@IsWellOrder.toIsSuccArchimedean = @IsWellOrder.toIsSuccArchimedean.proof_1

theorem Succ.rec_bot {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] [inst : SuccOrder α] [inst : IsSuccArchimedean α] (p : α → Prop) (hbot : p ⊥) (hsucc : (a : α) → p a → p (Order.succ a)) (a : α) :

p a

theorem Pred.rec_top {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] [inst : PredOrder α] [inst : IsPredArchimedean α] (p : α → Prop) (htop : p ⊤) (hpred : (a : α) → p a → p (Order.pred a)) (a : α) :

p a