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 #

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.succx = 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 aIsMax a
  • Proof that succ satifies ordering invariants betweeen LT and LE

    succ_le_of_lt : ∀ {a b : α}, a < bsucc a b
  • Proof that succ satifies ordering invariants betweeen LE and LT

    le_of_lt_succ : ∀ {a b : α}, a < succ ba b

Order equipped with a sensible successor function.

Instances
    theorem PredOrder.ext {α : Type u_1} :
    ∀ {inst : Preorder α} (x y : PredOrder α), PredOrder.pred = PredOrder.predx = 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 aIsMin a
    • Proof that pred satifies ordering invariants betweeen LT and LE

      le_pred_of_lt : ∀ {a b : α}, a < ba pred b
    • Proof that pred satifies ordering invariants betweeen LE and LT

      le_of_pred_lt : ∀ {a b : α}, pred a < ba b

    Order equipped with a sensible predecessor function.

    Instances
      instance instPredOrderOrderDualPreorder {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] :
      Equations
      • One or more equations did not get rendered due to their size.
      instance instSuccOrderOrderDualPreorder {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] :
      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 ba 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 < ba 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 asucc 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 asucc 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 apred 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 apred 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 : α) :
      theorem Order.max_of_succ_le {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} :
      Order.succ a aIsMax a
      theorem Order.succ_le_of_lt {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} :
      a < bOrder.succ a b
      theorem Order.le_of_lt_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} :
      a < Order.succ ba b
      @[simp]
      theorem Order.succ_le_iff_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} :
      @[simp]
      theorem Order.lt_succ_iff_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} :
      theorem Order.lt_succ_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} :
      ¬IsMax aa < 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 : α) :
      theorem Order.covby_succ_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} (h : ¬IsMax a) :
      theorem Order.lt_succ_iff_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) :
      theorem Order.succ_le_iff_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) :
      theorem Order.succ_lt_succ_iff_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) (hb : ¬IsMax 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) :
      @[simp]
      theorem Order.succ_le_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (h : a 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 : α) :
      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) :
      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) :
      theorem Order.Iio_succ_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} (ha : ¬IsMax a) :
      theorem Order.Ici_succ_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} (ha : ¬IsMax a) :
      theorem Order.Ico_succ_right_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (hb : ¬IsMax b) :
      theorem Order.Ioo_succ_right_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (hb : ¬IsMax b) :
      theorem Order.Icc_succ_left_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) :
      theorem Order.Ico_succ_left_of_not_isMax {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) :
      theorem Order.lt_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) :
      @[simp]
      theorem Order.lt_succ_iff {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :
      @[simp]
      theorem Order.succ_le_iff {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :
      theorem Order.succ_le_succ_iff {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :
      theorem Order.succ_lt_succ_iff {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :
      theorem Order.le_of_succ_le_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

      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 < bOrder.succ a < Order.succ b

      Alias of the reverse direction of Order.succ_lt_succ_iff.

      theorem Order.lt_of_succ_lt_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :
      Order.succ a < Order.succ ba < 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 : α) :
      @[simp]
      theorem Order.Iio_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) :
      @[simp]
      theorem Order.Ici_succ {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) :
      @[simp]
      theorem Order.Ico_succ_right {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) (b : α) :
      @[simp]
      theorem Order.Ioo_succ_right {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) (b : α) :
      @[simp]
      theorem Order.Icc_succ_left {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) (b : α) :
      @[simp]
      theorem Order.Ico_succ_left {α : Type u_1} [inst : Preorder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) (b : α) :
      @[simp]
      theorem Order.succ_eq_iff_isMax {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} :
      theorem IsMax.succ_eq {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} :
      IsMax aOrder.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) :
      theorem Order.le_le_succ_iff {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} :
      theorem Order.Covby.succ_eq {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} (h : a b) :
      theorem Order.Wcovby.le_succ {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} (h : a ⩿ b) :
      theorem Order.le_succ_iff_eq_or_le {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {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 : α) :
      theorem Order.Icc_succ_right {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} (h : a Order.succ b) :
      theorem Order.Ioc_succ_right {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} (h : a < Order.succ b) :
      theorem Order.Iio_succ_eq_insert_of_not_isMax {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} (h : ¬IsMax 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) :
      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) :
      @[simp]
      theorem Order.succ_eq_succ_iff {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :
      theorem Order.succ_injective {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : NoMaxOrder α] :
      theorem Order.succ_ne_succ_iff {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :
      theorem Order.succ_ne_succ {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] :

      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 α] :
      theorem Order.Iio_succ_eq_insert {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : NoMaxOrder α] (a : α) :
      theorem Order.Ico_succ_right_eq_insert {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] (h : a b) :
      theorem Order.Ioo_succ_right_eq_insert {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} {b : α} [inst : NoMaxOrder α] (h : a < b) :
      @[simp]
      theorem Order.succ_top {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : OrderTop α] :
      theorem Order.succ_le_iff_eq_top {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} [inst : OrderTop α] :
      theorem Order.lt_succ_iff_ne_top {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} [inst : OrderTop α] :
      theorem Order.lt_succ_bot_iff {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} [inst : OrderBot α] [inst : NoMaxOrder α] :
      theorem Order.le_succ_bot_iff {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] {a : α} [inst : OrderBot α] :
      theorem Order.bot_lt_succ {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : OrderBot α] [inst : Nontrivial α] (a : α) :
      theorem Order.succ_ne_bot {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : OrderBot α] [inst : Nontrivial α] (a : α) :
      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 : α) :
      theorem Order.min_of_le_pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} :
      a Order.pred aIsMin a
      theorem Order.le_pred_of_lt {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} :
      a < ba Order.pred b
      theorem Order.le_of_pred_lt {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} :
      Order.pred a < ba b
      @[simp]
      theorem Order.le_pred_iff_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} :
      @[simp]
      theorem Order.pred_lt_iff_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} :
      theorem Order.pred_lt_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} :
      ¬IsMin aOrder.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 : α) :
      theorem Order.pred_covby_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} (h : ¬IsMin a) :
      theorem Order.pred_lt_iff_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :
      theorem Order.le_pred_iff_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :
      @[simp]
      theorem Order.pred_le_pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (h : a 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 : α) :
      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) :
      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) :
      theorem Order.Ioi_pred_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} (ha : ¬IsMin a) :
      theorem Order.Iic_pred_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} (ha : ¬IsMin a) :
      theorem Order.Ioc_pred_left_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :
      theorem Order.Ioo_pred_left_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :
      theorem Order.Icc_pred_right_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin b) :
      theorem Order.Ioc_pred_right_of_not_isMin {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} (ha : ¬IsMin b) :
      theorem Order.pred_lt {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) :
      @[simp]
      theorem Order.pred_lt_iff {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :
      @[simp]
      theorem Order.le_pred_iff {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :
      theorem Order.pred_le_pred_iff {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :
      theorem Order.pred_lt_pred_iff {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :
      theorem Order.le_of_pred_le_pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

      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 ba < 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 < bOrder.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 : α) :
      @[simp]
      theorem Order.Ioi_pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) :
      @[simp]
      theorem Order.Iic_pred {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) :
      @[simp]
      theorem Order.Ioc_pred_left {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) (b : α) :
      @[simp]
      theorem Order.Ioo_pred_left {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) (b : α) :
      @[simp]
      theorem Order.Icc_pred_right {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) (b : α) :
      @[simp]
      theorem Order.Ioc_pred_right {α : Type u_1} [inst : Preorder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) (b : α) :
      @[simp]
      theorem Order.pred_eq_iff_isMin {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} :
      theorem IsMin.pred_eq {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} :
      IsMin aOrder.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 : α} :
      theorem Order.Covby.pred_eq {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} (h : a b) :
      theorem Order.Wcovby.pred_le {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} (h : a ⩿ b) :
      theorem Order.pred_le_iff_eq_or_le {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {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 : α) :
      theorem Order.Ioi_pred_eq_insert_of_not_isMin {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} (ha : ¬IsMin a) :
      theorem Order.Icc_pred_left {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} (h : Order.pred a b) :
      theorem Order.Ico_pred_left {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} (h : Order.pred a < b) :
      @[simp]
      theorem Order.pred_eq_pred_iff {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :
      theorem Order.pred_injective {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] [inst : NoMinOrder α] :
      theorem Order.pred_ne_pred_iff {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :
      theorem Order.pred_ne_pred {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] :

      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 α] :
      theorem Order.Ioi_pred_eq_insert {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) :
      theorem Order.Ico_pred_right_eq_insert {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] (h : a b) :
      theorem Order.Ioo_pred_right_eq_insert {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} {b : α} [inst : NoMinOrder α] (h : a < b) :
      @[simp]
      theorem Order.pred_bot {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] [inst : OrderBot α] :
      theorem Order.le_pred_iff_eq_bot {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} [inst : OrderBot α] :
      theorem Order.pred_lt_iff_ne_bot {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} [inst : OrderBot α] :
      theorem Order.pred_top_lt_iff {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} [inst : OrderTop α] [inst : NoMinOrder α] :
      theorem Order.pred_top_le_iff {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] {a : α} [inst : OrderTop α] :
      theorem Order.pred_lt_top {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] [inst : OrderTop α] [inst : Nontrivial α] (a : α) :
      theorem Order.pred_ne_top {α : Type u_1} [inst : PartialOrder α] [inst : PredOrder α] [inst : OrderTop α] [inst : Nontrivial α] (a : α) :
      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) :
      @[simp]
      theorem Order.pred_succ_of_not_isMax {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : PredOrder α] {a : α} (h : ¬IsMax a) :
      theorem Order.succ_pred {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : PredOrder α] [inst : NoMinOrder α] (a : α) :
      theorem Order.pred_succ {α : Type u_1} [inst : PartialOrder α] [inst : SuccOrder α] [inst : PredOrder α] [inst : NoMaxOrder α] (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)) :
      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)) :

      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 #

      instance WithTop.instSuccOrderWithTopPreorderToPreorder {α : Type u_1} [inst : DecidableEq α] [inst : PartialOrder α] [inst : OrderTop α] [inst : SuccOrder α] :
      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 α] :
      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 α] :
      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 α] :
      @[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 ) :

      Adding a ⊤⊤ to a NoMaxOrder #

      instance WithTop.succOrderOfNoMaxOrder {α : Type u_1} [inst : Preorder α] [inst : NoMaxOrder α] [inst : SuccOrder α] :
      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)

      Adding a ⊥⊥ to an OrderBot #

      instance WithBot.instSuccOrderWithBotPreorder {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] [inst : SuccOrder α] :
      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 α] :
      @[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 ) :
      instance WithBot.instPredOrderWithBotPreorderToPreorder {α : Type u_1} [inst : DecidableEq α] [inst : PartialOrder α] [inst : OrderBot α] [inst : PredOrder α] :
      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 α] :
      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.predOrderOfNoMinOrder {α : Type u_1} [inst : Preorder α] [inst : NoMinOrder α] [inst : PredOrder α] :
      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 bn, (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 bn, (Order.pred^[n]) b = a

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

        Instances
          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 nP nP (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
          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 mP nP (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
          theorem Succ.rec_bot {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] [inst : SuccOrder α] [inst : IsSuccArchimedean α] (p : αProp) (hbot : p ) (hsucc : (a : α) → p ap (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 ap (Order.pred a)) (a : α) :
          p a