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 α] where
  (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 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 α.

theorem SuccOrder.ext {α : Type u_3} :
∀ {inst : Preorder α} {x y : SuccOrder α}, SuccOrder.succ = SuccOrder.succx = y
theorem SuccOrder.ext_iff {α : Type u_3} :
∀ {inst : Preorder α} {x y : SuccOrder α}, x = y SuccOrder.succ = SuccOrder.succ
class SuccOrder (α : Type u_3) [Preorder α] :
Type u_3

Order equipped with a sensible successor function.

  • succ : αα

    Successor function

  • le_succ : ∀ (a : α), a SuccOrder.succ a

    Proof of basic ordering with respect to succ

  • max_of_succ_le : ∀ {a : α}, SuccOrder.succ a aIsMax a

    Proof of interaction between succ and maximal element

  • succ_le_of_lt : ∀ {a b : α}, a < bSuccOrder.succ a b

    Proof that succ a is the least element greater than a

Instances
    theorem SuccOrder.le_succ {α : Type u_3} :
    ∀ {inst : Preorder α} [self : SuccOrder α] (a : α), a SuccOrder.succ a

    Proof of basic ordering with respect to succ

    theorem SuccOrder.max_of_succ_le {α : Type u_3} :
    ∀ {inst : Preorder α} [self : SuccOrder α] {a : α}, SuccOrder.succ a aIsMax a

    Proof of interaction between succ and maximal element

    theorem SuccOrder.succ_le_of_lt {α : Type u_3} :
    ∀ {inst : Preorder α} [self : SuccOrder α] {a b : α}, a < bSuccOrder.succ a b

    Proof that succ a is the least element greater than a

    theorem PredOrder.ext {α : Type u_3} :
    ∀ {inst : Preorder α} {x y : PredOrder α}, PredOrder.pred = PredOrder.predx = y
    theorem PredOrder.ext_iff {α : Type u_3} :
    ∀ {inst : Preorder α} {x y : PredOrder α}, x = y PredOrder.pred = PredOrder.pred
    class PredOrder (α : Type u_3) [Preorder α] :
    Type u_3

    Order equipped with a sensible predecessor function.

    • pred : αα

      Predecessor function

    • pred_le : ∀ (a : α), PredOrder.pred a a

      Proof of basic ordering with respect to pred

    • min_of_le_pred : ∀ {a : α}, a PredOrder.pred aIsMin a

      Proof of interaction between pred and minimal element

    • le_pred_of_lt : ∀ {a b : α}, a < ba PredOrder.pred b

      Proof that pred b is the greatest element less than b

    Instances
      theorem PredOrder.pred_le {α : Type u_3} :
      ∀ {inst : Preorder α} [self : PredOrder α] (a : α), PredOrder.pred a a

      Proof of basic ordering with respect to pred

      theorem PredOrder.min_of_le_pred {α : Type u_3} :
      ∀ {inst : Preorder α} [self : PredOrder α] {a : α}, a PredOrder.pred aIsMin a

      Proof of interaction between pred and minimal element

      theorem PredOrder.le_pred_of_lt {α : Type u_3} :
      ∀ {inst : Preorder α} [self : PredOrder α] {a b : α}, a < ba PredOrder.pred b

      Proof that pred b is the greatest element less than b

      Equations
      • instPredOrderOrderDualOfSuccOrder = { pred := OrderDual.toDual SuccOrder.succ OrderDual.ofDual, pred_le := , min_of_le_pred := , le_pred_of_lt := }
      Equations
      • instSuccOrderOrderDualOfPredOrder = { succ := OrderDual.toDual PredOrder.pred OrderDual.ofDual, le_succ := , max_of_succ_le := , succ_le_of_lt := }
      def SuccOrder.ofSuccLeIff {α : Type u_1} [Preorder α] (succ : αα) (hsucc_le_iff : ∀ {a b : α}, succ a b a < b) :

      A constructor for SuccOrder α usable when α has no maximal element.

      Equations
      • SuccOrder.ofSuccLeIff succ hsucc_le_iff = { succ := succ, le_succ := , max_of_succ_le := , succ_le_of_lt := }
      Instances For
        def PredOrder.ofLePredIff {α : Type u_1} [Preorder α] (pred : αα) (hle_pred_iff : ∀ {a b : α}, a pred b a < b) :

        A constructor for PredOrder α usable when α has no minimal element.

        Equations
        • PredOrder.ofLePredIff pred hle_pred_iff = { pred := pred, pred_le := , min_of_le_pred := , le_pred_of_lt := }
        Instances For
          @[simp]
          theorem SuccOrder.ofCore_succ {α : Type u_1} [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} [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
          • SuccOrder.ofCore succ hn hm = { succ := succ, le_succ := , max_of_succ_le := , succ_le_of_lt := }
          Instances For
            @[simp]
            theorem PredOrder.ofCore_pred {α : Type u_1} [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} [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
            • PredOrder.ofCore pred hn hm = { pred := pred, pred_le := , min_of_le_pred := , le_pred_of_lt := }
            Instances For
              noncomputable def SuccOrder.ofLinearWellFoundedLT (α : Type u_1) [LinearOrder α] [WellFoundedLT α] :

              A well-order is a SuccOrder.

              Equations
              Instances For
                noncomputable def PredOrder.ofLinearWellFoundedGT (α : Type u_3) [LinearOrder α] [WellFoundedGT α] :

                A linear order with well-founded greater-than relation is a PredOrder.

                Equations
                Instances For

                  Successor order #

                  def Order.succ {α : Type u_1} [Preorder α] [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
                  Instances For
                    theorem Order.le_succ {α : Type u_1} [Preorder α] [SuccOrder α] (a : α) :
                    theorem Order.max_of_succ_le {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} :
                    Order.succ a aIsMax a
                    theorem Order.succ_le_of_lt {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} :
                    a < bOrder.succ a b
                    theorem LT.lt.succ_le {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} :
                    a < bOrder.succ a b

                    Alias of Order.succ_le_of_lt.

                    @[simp]
                    theorem Order.succ_le_iff_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} :
                    theorem IsMax.of_succ_le {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} :
                    Order.succ a aIsMax a

                    Alias of the forward direction of Order.succ_le_iff_isMax.

                    theorem IsMax.succ_le {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} :
                    IsMax aOrder.succ a a

                    Alias of the reverse direction of Order.succ_le_iff_isMax.

                    @[simp]
                    theorem Order.lt_succ_iff_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} :
                    theorem Order.lt_succ_of_not_isMax {α : Type u_1} [Preorder α] [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} [Preorder α] [SuccOrder α] (a : α) :
                    theorem Order.covBy_succ_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} (h : ¬IsMax a) :
                    theorem Order.lt_succ_of_le_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} (hab : b a) (ha : ¬IsMax a) :
                    theorem Order.succ_le_iff_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) :
                    theorem Order.succ_lt_succ_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} (h : a < b) (hb : ¬IsMax b) :
                    @[simp]
                    theorem Order.succ_le_succ {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} (h : a b) :
                    theorem Order.succ_mono {α : Type u_1} [Preorder α] [SuccOrder α] :
                    Monotone Order.succ
                    theorem Order.le_succ_of_wcovBy {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} (h : a ⩿ b) :

                    See also Order.succ_eq_of_covBy.

                    theorem WCovBy.le_succ {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} (h : a ⩿ b) :

                    Alias of Order.le_succ_of_wcovBy.


                    See also Order.succ_eq_of_covBy.

                    theorem Order.le_succ_iterate {α : Type u_1} [Preorder α] [SuccOrder α] (k : ) (x : α) :
                    x Order.succ^[k] x
                    theorem Order.isMax_iterate_succ_of_eq_of_lt {α : Type u_1} [Preorder α] [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} [Preorder α] [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.Ici_succ_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} (ha : ¬IsMax a) :
                    theorem Order.Icc_subset_Ico_succ_right_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} (hb : ¬IsMax b) :
                    theorem Order.Ioc_subset_Ioo_succ_right_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} (hb : ¬IsMax b) :
                    theorem Order.Icc_succ_left_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) :
                    theorem Order.Ico_succ_left_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) :
                    theorem Order.lt_succ {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) :
                    @[simp]
                    theorem Order.lt_succ_of_le {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] :
                    a ba < Order.succ b
                    @[simp]
                    theorem Order.succ_le_iff {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] :
                    theorem Order.succ_lt_succ {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] (hab : a < b) :
                    theorem Order.succ_strictMono {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] :
                    StrictMono Order.succ
                    theorem Order.covBy_succ {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) :
                    @[simp]
                    theorem Order.Iic_subset_Iio_succ {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) :
                    @[simp]
                    theorem Order.Ici_succ {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) :
                    @[simp]
                    theorem Order.Icc_subset_Ico_succ_right {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) (b : α) :
                    @[simp]
                    theorem Order.Ioc_subset_Ioo_succ_right {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) (b : α) :
                    @[simp]
                    theorem Order.Icc_succ_left {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) (b : α) :
                    @[simp]
                    theorem Order.Ico_succ_left {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) (b : α) :
                    @[simp]
                    theorem Order.succ_eq_iff_isMax {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} :
                    theorem IsMax.succ_eq {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} :
                    IsMax aOrder.succ a = a

                    Alias of the reverse direction of Order.succ_eq_iff_isMax.

                    theorem Order.le_le_succ_iff {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} {b : α} :
                    theorem Order.succ_eq_of_covBy {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} {b : α} (h : a b) :

                    See also Order.le_succ_of_wcovBy.

                    theorem CovBy.succ_eq {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} {b : α} (h : a b) :

                    Alias of Order.succ_eq_of_covBy.


                    See also Order.le_succ_of_wcovBy.

                    theorem OrderIso.map_succ {α : Type u_1} [PartialOrder α] [SuccOrder α] {β : Type u_3} [PartialOrder β] [SuccOrder β] (f : α ≃o β) (a : α) :
                    f (Order.succ a) = Order.succ (f a)
                    theorem Order.succ_eq_iff_covBy {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] :
                    @[simp]
                    theorem Order.succ_top {α : Type u_1} [PartialOrder α] [SuccOrder α] [OrderTop α] :
                    theorem Order.succ_le_iff_eq_top {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} [OrderTop α] :
                    theorem Order.lt_succ_iff_ne_top {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} [OrderTop α] :
                    theorem Order.bot_lt_succ {α : Type u_1} [PartialOrder α] [SuccOrder α] [OrderBot α] [Nontrivial α] (a : α) :
                    theorem Order.succ_ne_bot {α : Type u_1} [PartialOrder α] [SuccOrder α] [OrderBot α] [Nontrivial α] (a : α) :
                    theorem Order.le_of_lt_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} :
                    a < Order.succ ba b
                    theorem Order.lt_succ_iff_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) :
                    theorem Order.succ_lt_succ_iff_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) (hb : ¬IsMax b) :
                    theorem Order.succ_le_succ_iff_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) (hb : ¬IsMax b) :
                    theorem Order.Iio_succ_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} (ha : ¬IsMax a) :
                    theorem Order.Ico_succ_right_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} (hb : ¬IsMax b) :
                    theorem Order.Ioo_succ_right_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} (hb : ¬IsMax b) :
                    theorem Order.succ_eq_succ_iff_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} (ha : ¬IsMax a) (hb : ¬IsMax b) :
                    theorem Order.le_succ_iff_eq_or_le {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} :
                    theorem Order.lt_succ_iff_eq_or_lt_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} (hb : ¬IsMax b) :
                    a < Order.succ b a = b a < b
                    theorem Order.not_isMin_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] [Nontrivial α] (a : α) :
                    theorem Order.Iic_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] (a : α) :
                    theorem Order.Icc_succ_right {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} (h : a Order.succ b) :
                    theorem Order.Ioc_succ_right {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} (h : a < Order.succ b) :
                    theorem Order.Ico_succ_right_eq_insert_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} (h₁ : a b) (h₂ : ¬IsMax b) :
                    theorem Order.Ioo_succ_right_eq_insert_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} (h₁ : a < b) (h₂ : ¬IsMax b) :
                    @[simp]
                    theorem Order.lt_succ_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] :
                    theorem Order.succ_le_succ_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] :
                    theorem Order.succ_lt_succ_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] :
                    theorem Order.le_of_succ_le_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] :

                    Alias of the forward direction of Order.succ_le_succ_iff.

                    theorem Order.lt_of_succ_lt_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] :
                    Order.succ a < Order.succ ba < b

                    Alias of the forward direction of Order.succ_lt_succ_iff.

                    @[simp]
                    theorem Order.Iio_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a : α) :
                    @[simp]
                    theorem Order.Ico_succ_right {α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a : α) (b : α) :
                    @[simp]
                    theorem Order.Ioo_succ_right {α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a : α) (b : α) :
                    @[simp]
                    theorem Order.succ_eq_succ_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] :
                    theorem Order.succ_ne_succ_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] :
                    theorem Order.succ_ne_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] :

                    Alias of the reverse direction of Order.succ_ne_succ_iff.

                    theorem Order.lt_succ_iff_eq_or_lt {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] :
                    a < Order.succ b a = b a < b
                    theorem Order.Ico_succ_right_eq_insert {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] (h : a b) :
                    theorem Order.Ioo_succ_right_eq_insert {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} {b : α} [NoMaxOrder α] (h : a < b) :
                    theorem Order.lt_succ_bot_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} [OrderBot α] [NoMaxOrder α] :

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

                    Equations
                    • =
                    theorem Order.succ_eq_sInf {α : Type u_1} [CompleteLattice α] [SuccOrder α] (a : α) :
                    theorem Order.succ_eq_iInf {α : Type u_1} [CompleteLattice α] [SuccOrder α] (a : α) :
                    Order.succ a = ⨅ (b : α), ⨅ (_ : b > a), b

                    Predecessor order #

                    def Order.pred {α : Type u_1} [Preorder α] [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
                    Instances For
                      theorem Order.pred_le {α : Type u_1} [Preorder α] [PredOrder α] (a : α) :
                      theorem Order.min_of_le_pred {α : Type u_1} [Preorder α] [PredOrder α] {a : α} :
                      a Order.pred aIsMin a
                      theorem Order.le_pred_of_lt {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} :
                      a < ba Order.pred b
                      theorem LT.lt.le_pred {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} :
                      a < ba Order.pred b

                      Alias of Order.le_pred_of_lt.

                      @[simp]
                      theorem Order.le_pred_iff_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} :
                      theorem IsMin.le_pred {α : Type u_1} [Preorder α] [PredOrder α] {a : α} :
                      IsMin aa Order.pred a

                      Alias of the reverse direction of Order.le_pred_iff_isMin.

                      theorem IsMin.of_le_pred {α : Type u_1} [Preorder α] [PredOrder α] {a : α} :
                      a Order.pred aIsMin a

                      Alias of the forward direction of Order.le_pred_iff_isMin.

                      @[simp]
                      theorem Order.pred_lt_iff_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} :
                      theorem Order.pred_lt_of_not_isMin {α : Type u_1} [Preorder α] [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} [Preorder α] [PredOrder α] (a : α) :
                      theorem Order.pred_covBy_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} (h : ¬IsMin a) :
                      theorem Order.pred_lt_of_not_isMin_of_le {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :
                      a bOrder.pred a < b
                      theorem Order.le_pred_iff_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :
                      theorem Order.pred_lt_pred_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} (h : a < b) (ha : ¬IsMin a) :
                      theorem Order.pred_le_pred_of_not_isMin_of_le {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) (hb : ¬IsMin b) :
                      @[simp]
                      theorem Order.pred_le_pred {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} (h : a b) :
                      theorem Order.pred_mono {α : Type u_1} [Preorder α] [PredOrder α] :
                      Monotone Order.pred
                      theorem Order.pred_le_of_wcovBy {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} (h : a ⩿ b) :

                      See also Order.pred_eq_of_covBy.

                      theorem WCovBy.pred_le {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} (h : a ⩿ b) :

                      Alias of Order.pred_le_of_wcovBy.


                      See also Order.pred_eq_of_covBy.

                      theorem Order.pred_iterate_le {α : Type u_1} [Preorder α] [PredOrder α] (k : ) (x : α) :
                      Order.pred^[k] x x
                      theorem Order.isMin_iterate_pred_of_eq_of_lt {α : Type u_1} [Preorder α] [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} [Preorder α] [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.Iic_pred_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} (ha : ¬IsMin a) :
                      theorem Order.Icc_subset_Ioc_pred_left_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :
                      theorem Order.Ico_subset_Ioo_pred_left_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :
                      theorem Order.Icc_pred_right_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin b) :
                      theorem Order.Ioc_pred_right_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin b) :
                      theorem Order.pred_lt {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) :
                      @[simp]
                      theorem Order.pred_lt_of_le {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :
                      a bOrder.pred a < b
                      @[simp]
                      theorem Order.le_pred_iff {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :
                      theorem Order.pred_le_pred_of_le {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :
                      theorem Order.pred_lt_pred {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :
                      a < bOrder.pred a < Order.pred b
                      theorem Order.pred_strictMono {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] :
                      StrictMono Order.pred
                      theorem Order.pred_covBy {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) :
                      @[simp]
                      theorem Order.Ici_subset_Ioi_pred {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) :
                      @[simp]
                      theorem Order.Iic_pred {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) :
                      @[simp]
                      theorem Order.Icc_subset_Ioc_pred_left {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) (b : α) :
                      @[simp]
                      theorem Order.Ico_subset_Ioo_pred_left {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) (b : α) :
                      @[simp]
                      theorem Order.Icc_pred_right {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) (b : α) :
                      @[simp]
                      theorem Order.Ioc_pred_right {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) (b : α) :
                      @[simp]
                      theorem Order.pred_eq_iff_isMin {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} :
                      theorem IsMin.pred_eq {α : Type u_1} [PartialOrder α] [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} [PartialOrder α] [PredOrder α] {a : α} {b : α} :
                      theorem Order.pred_eq_of_covBy {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} {b : α} (h : a b) :

                      See also Order.pred_le_of_wcovBy.

                      theorem CovBy.pred_eq {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} {b : α} (h : a b) :

                      Alias of Order.pred_eq_of_covBy.


                      See also Order.pred_le_of_wcovBy.

                      theorem OrderIso.map_pred {α : Type u_1} [PartialOrder α] [PredOrder α] {β : Type u_3} [PartialOrder β] [PredOrder β] (f : α ≃o β) (a : α) :
                      f (Order.pred a) = Order.pred (f a)
                      theorem Order.pred_eq_iff_covBy {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :
                      @[simp]
                      theorem Order.pred_bot {α : Type u_1} [PartialOrder α] [PredOrder α] [OrderBot α] :
                      theorem Order.le_pred_iff_eq_bot {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} [OrderBot α] :
                      theorem Order.pred_lt_iff_ne_bot {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} [OrderBot α] :
                      theorem Order.pred_lt_top {α : Type u_1} [PartialOrder α] [PredOrder α] [OrderTop α] [Nontrivial α] (a : α) :
                      theorem Order.pred_ne_top {α : Type u_1} [PartialOrder α] [PredOrder α] [OrderTop α] [Nontrivial α] (a : α) :
                      theorem Order.le_of_pred_lt {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} :
                      Order.pred a < ba b
                      theorem Order.pred_lt_iff_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :
                      theorem Order.pred_lt_pred_iff_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) (hb : ¬IsMin b) :
                      theorem Order.pred_le_pred_iff_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) (hb : ¬IsMin b) :
                      theorem Order.Ioi_pred_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} (ha : ¬IsMin a) :
                      theorem Order.Ioc_pred_left_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :
                      theorem Order.Ioo_pred_left_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :
                      theorem Order.pred_eq_pred_iff_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) (hb : ¬IsMin b) :
                      theorem Order.pred_le_iff_eq_or_le {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} :
                      theorem Order.pred_lt_iff_eq_or_lt_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} (ha : ¬IsMin a) :
                      Order.pred a < b a = b a < b
                      theorem Order.not_isMax_pred {α : Type u_1} [LinearOrder α] [PredOrder α] [Nontrivial α] (a : α) :
                      theorem Order.Ici_pred {α : Type u_1} [LinearOrder α] [PredOrder α] (a : α) :
                      theorem Order.Icc_pred_left {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} (h : Order.pred a b) :
                      theorem Order.Ico_pred_left {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} (h : Order.pred a < b) :
                      @[simp]
                      theorem Order.pred_lt_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :
                      theorem Order.pred_le_pred_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :
                      theorem Order.pred_lt_pred_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :
                      theorem Order.le_of_pred_le_pred {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :

                      Alias of the forward direction of Order.pred_le_pred_iff.

                      theorem Order.lt_of_pred_lt_pred {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :
                      Order.pred a < Order.pred ba < b

                      Alias of the forward direction of Order.pred_lt_pred_iff.

                      @[simp]
                      theorem Order.Ioi_pred {α : Type u_1} [LinearOrder α] [PredOrder α] [NoMinOrder α] (a : α) :
                      @[simp]
                      theorem Order.Ioc_pred_left {α : Type u_1} [LinearOrder α] [PredOrder α] [NoMinOrder α] (a : α) (b : α) :
                      @[simp]
                      theorem Order.Ioo_pred_left {α : Type u_1} [LinearOrder α] [PredOrder α] [NoMinOrder α] (a : α) (b : α) :
                      @[simp]
                      theorem Order.pred_eq_pred_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :
                      theorem Order.pred_ne_pred_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :
                      theorem Order.pred_ne_pred {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :

                      Alias of the reverse direction of Order.pred_ne_pred_iff.

                      theorem Order.pred_lt_iff_eq_or_lt {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] :
                      Order.pred a < b a = b a < b
                      theorem Order.Ico_pred_right_eq_insert {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] (h : a b) :
                      theorem Order.Ioo_pred_right_eq_insert {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} {b : α} [NoMinOrder α] (h : a < b) :
                      theorem Order.pred_top_lt_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} [OrderTop α] [NoMinOrder α] :

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

                      Equations
                      • =
                      theorem Order.pred_eq_sSup {α : Type u_1} [CompleteLattice α] [PredOrder α] (a : α) :
                      theorem Order.pred_eq_iSup {α : Type u_1} [CompleteLattice α] [PredOrder α] (a : α) :
                      Order.pred a = ⨆ (b : α), ⨆ (_ : b < a), b

                      Successor-predecessor orders #

                      theorem Order.le_succ_pred {α : Type u_1} [Preorder α] [SuccOrder α] [PredOrder α] (a : α) :
                      theorem Order.pred_succ_le {α : Type u_1} [Preorder α] [SuccOrder α] [PredOrder α] (a : α) :
                      theorem Order.pred_le_iff_le_succ {α : Type u_1} [Preorder α] [SuccOrder α] [PredOrder α] {a : α} {b : α} :
                      theorem Order.gc_pred_succ {α : Type u_1} [Preorder α] [SuccOrder α] [PredOrder α] :
                      GaloisConnection Order.pred Order.succ
                      @[simp]
                      theorem Order.succ_pred_of_not_isMin {α : Type u_1} [PartialOrder α] [SuccOrder α] [PredOrder α] {a : α} (h : ¬IsMin a) :
                      @[simp]
                      theorem Order.pred_succ_of_not_isMax {α : Type u_1} [PartialOrder α] [SuccOrder α] [PredOrder α] {a : α} (h : ¬IsMax a) :
                      theorem Order.succ_pred {α : Type u_1} [PartialOrder α] [SuccOrder α] [PredOrder α] [NoMinOrder α] (a : α) :
                      theorem Order.pred_succ {α : Type u_1} [PartialOrder α] [SuccOrder α] [PredOrder α] [NoMaxOrder α] (a : α) :
                      theorem Order.pred_succ_iterate_of_not_isMax {α : Type u_1} [PartialOrder α] [SuccOrder α] [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} [PartialOrder α] [SuccOrder α] [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 #

                      Equations
                      • One or more equations did not get rendered due to their size.
                      @[simp]
                      theorem WithTop.succ_coe_of_isMax {α : Type u_1} [DecidableEq α] [PartialOrder α] [SuccOrder α] {a : α} (h : IsMax a) :
                      theorem WithTop.succ_coe_of_not_isMax {α : Type u_1} [DecidableEq α] [PartialOrder α] [SuccOrder α] {a : α} (h : ¬IsMax a) :
                      Order.succ a = (Order.succ a)
                      @[simp]
                      theorem WithTop.succ_coe {α : Type u_1} [DecidableEq α] [PartialOrder α] [SuccOrder α] [NoMaxOrder α] {a : α} :
                      Order.succ a = (Order.succ a)
                      instance WithTop.instPredOrder {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] :
                      Equations
                      • WithTop.instPredOrder = { pred := fun (a : WithTop α) => match a with | none => | some a => (Order.pred a), pred_le := , min_of_le_pred := , le_pred_of_lt := }
                      @[simp]
                      theorem WithTop.pred_top {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] :
                      @[simp]
                      theorem WithTop.pred_coe {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] (a : α) :
                      Order.pred a = (Order.pred a)
                      @[simp]
                      theorem WithTop.pred_untop {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] (a : WithTop α) (ha : a ) :
                      Order.pred (a.untop ha) = (Order.pred a).untop
                      Equations
                      • =

                      Adding a to an OrderBot #

                      instance WithBot.instSuccOrder {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] :
                      Equations
                      • WithBot.instSuccOrder = { succ := fun (a : WithBot α) => match a with | none => | some a => (Order.succ a), le_succ := , max_of_succ_le := , succ_le_of_lt := }
                      @[simp]
                      theorem WithBot.succ_bot {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] :
                      @[simp]
                      theorem WithBot.succ_coe {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] (a : α) :
                      Order.succ a = (Order.succ a)
                      @[simp]
                      theorem WithBot.succ_unbot {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] (a : WithBot α) (ha : a ) :
                      Order.succ (a.unbot ha) = (Order.succ a).unbot
                      Equations
                      • One or more equations did not get rendered due to their size.
                      @[simp]
                      theorem WithBot.pred_coe_of_isMin {α : Type u_1} [DecidableEq α] [PartialOrder α] [PredOrder α] {a : α} (h : IsMin a) :
                      theorem WithBot.pred_coe_of_not_isMin {α : Type u_1} [DecidableEq α] [PartialOrder α] [PredOrder α] {a : α} (h : ¬IsMin a) :
                      Order.pred a = (Order.pred a)
                      theorem WithBot.pred_coe {α : Type u_1} [DecidableEq α] [PartialOrder α] [PredOrder α] [NoMinOrder α] {a : α} :
                      Order.pred a = (Order.pred a)

                      Adding a to a NoMinOrder #

                      Equations
                      • =
                      @[reducible, inline]
                      abbrev SuccOrder.ofOrderIso {X : Type u_3} {Y : Type u_4} [Preorder X] [Preorder Y] [SuccOrder X] (f : X ≃o Y) :

                      SuccOrder transfers across equivalences between orders.

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev PredOrder.ofOrderIso {X : Type u_3} {Y : Type u_4} [Preorder X] [Preorder Y] [PredOrder X] (f : X ≃o Y) :

                        PredOrder transfers across equivalences between orders.

                        Equations
                        Instances For
                          noncomputable instance Set.OrdConnected.predOrder {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [PredOrder α] :
                          Equations
                          • Set.OrdConnected.predOrder = { pred := fun (x : s) => if h : Order.pred x s then Order.pred x, h else x, pred_le := , min_of_le_pred := , le_pred_of_lt := }
                          @[simp]
                          theorem coe_pred_of_mem {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [PredOrder α] {a : s} (h : Order.pred a s) :
                          (Order.pred a) = Order.pred a
                          theorem isMin_of_not_pred_mem {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [PredOrder α] {a : s} (h : Order.pred as) :
                          theorem not_pred_mem_iff_isMin {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [PredOrder α] [NoMinOrder α] {a : s} :
                          Order.pred as IsMin a
                          noncomputable instance Set.OrdConnected.succOrder {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [SuccOrder α] :
                          Equations
                          @[simp]
                          theorem coe_succ_of_mem {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [SuccOrder α] {a : s} (h : Order.succ a s) :
                          (Order.succ a) = Order.succ a
                          theorem isMax_of_not_succ_mem {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [SuccOrder α] {a : s} (h : Order.succ as) :
                          theorem not_succ_mem_iff_isMax {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [SuccOrder α] [NoMaxOrder α] {a : s} :
                          Order.succ as IsMax a