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 α.

class SuccOrder (α : Type u_3) [Preorder α] :
Type u_3

Order equipped with a sensible successor function.

  • succ : αα

    Successor function

  • le_succ (a : α) : a succ a

    Proof of basic ordering with respect to succ

  • max_of_succ_le {a : α} : succ a aIsMax a

    Proof of interaction between succ and maximal element

  • succ_le_of_lt {a b : α} : a < bsucc a b

    Proof that succ a is the least element greater than a

Instances
    theorem SuccOrder.ext_iff {α : Type u_3} {inst✝ : Preorder α} {x y : SuccOrder α} :
    theorem SuccOrder.ext {α : Type u_3} {inst✝ : Preorder α} {x y : SuccOrder α} (succ : succ = succ) :
    x = y
    class PredOrder (α : Type u_3) [Preorder α] :
    Type u_3

    Order equipped with a sensible predecessor function.

    • pred : αα

      Predecessor function

    • pred_le (a : α) : pred a a

      Proof of basic ordering with respect to pred

    • min_of_le_pred {a : α} : a pred aIsMin a

      Proof of interaction between pred and minimal element

    • le_pred_of_lt {a b : α} : a < ba pred b

      Proof that pred b is the greatest element less than b

    Instances
      theorem PredOrder.ext_iff {α : Type u_3} {inst✝ : Preorder α} {x y : PredOrder α} :
      theorem PredOrder.ext {α : Type u_3} {inst✝ : Preorder α} {x y : PredOrder α} (pred : pred = pred) :
      x = y
      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
        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
            Instances For
              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
                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 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
                    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✝
                      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
                                Instances For
                                  theorem Order.le_succ {α : Type u_1} [Preorder α] [SuccOrder α] (a : α) :
                                  a succ a
                                  theorem Order.max_of_succ_le {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} :
                                  succ a aIsMax a
                                  theorem Order.succ_le_of_lt {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} :
                                  a < bsucc 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 < succ a

                                  Alias of the reverse direction of Order.lt_succ_iff_not_isMax.

                                  theorem Order.wcovBy_succ {α : Type u_1} [Preorder α] [SuccOrder α] (a : α) :
                                  a ⩿ succ a
                                  theorem Order.covBy_succ_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} (h : ¬IsMax a) :
                                  a succ a
                                  theorem Order.lt_succ_of_le_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (hab : b a) (ha : ¬IsMax a) :
                                  b < succ a
                                  theorem Order.succ_le_iff_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) :
                                  succ a b a < b
                                  theorem Order.succ_lt_succ_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (h : a < b) (hb : ¬IsMax b) :
                                  succ a < succ b
                                  @[simp]
                                  theorem Order.succ_le_succ {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (h : a b) :
                                  theorem Order.le_succ_of_wcovBy {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (h : a ⩿ b) :
                                  b succ a

                                  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 : α) :
                                  theorem Order.isMax_iterate_succ_of_eq_of_lt {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {n m : } (h_eq : succ^[n] a = succ^[m] a) (h_lt : n < m) :
                                  theorem Order.isMax_iterate_succ_of_eq_of_ne {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {n m : } (h_eq : succ^[n] a = succ^[m] a) (h_ne : n m) :
                                  theorem Order.Iic_subset_Iio_succ_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} (ha : ¬IsMax 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) :
                                  Set.Icc (succ a) b = Set.Ioc a b
                                  theorem Order.Ico_succ_left_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) :
                                  Set.Ico (succ a) b = Set.Ioo a b
                                  theorem Order.lt_succ {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) :
                                  a < succ a
                                  @[simp]
                                  theorem Order.lt_succ_of_le {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} [NoMaxOrder α] :
                                  a ba < succ b
                                  @[simp]
                                  theorem Order.succ_le_iff {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} [NoMaxOrder α] :
                                  succ a b a < b
                                  theorem Order.succ_lt_succ {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (hab : a < b) :
                                  succ a < succ b
                                  theorem Order.covBy_succ {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) :
                                  a succ a
                                  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 : α) :
                                  Set.Icc (succ a) b = Set.Ioc a b
                                  @[simp]
                                  theorem Order.Ico_succ_left {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a b : α) :
                                  Set.Ico (succ a) b = Set.Ioo a b
                                  @[simp]
                                  theorem Order.succ_eq_iff_isMax {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} :
                                  succ a = a IsMax 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_iff_eq_or_succ_le {α : Type u_1} [PartialOrder α] [SuccOrder α] {a b : α} :
                                  a b a = b succ a b
                                  theorem Order.le_le_succ_iff {α : Type u_1} [PartialOrder α] [SuccOrder α] {a b : α} :
                                  a b b succ a b = a b = succ a
                                  theorem Order.succ_eq_of_covBy {α : Type u_1} [PartialOrder α] [SuccOrder α] {a b : α} (h : a b) :
                                  succ 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} {β : Type u_2} [PartialOrder α] [SuccOrder α] [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 α] :
                                  succ a = b a b
                                  @[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 α] :
                                  succ a a a =
                                  theorem Order.lt_succ_iff_ne_top {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} [OrderTop α] :
                                  a < succ a a
                                  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 < succ ba b
                                  theorem Order.lt_succ_iff_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) :
                                  b < succ a b a
                                  theorem Order.succ_lt_succ_iff_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) (hb : ¬IsMax b) :
                                  succ a < succ b a < b
                                  theorem Order.succ_le_succ_iff_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) (hb : ¬IsMax b) :
                                  succ a succ b a 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) :
                                  Set.Ico a (succ b) = Set.Icc a b
                                  theorem Order.Ioo_succ_right_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (hb : ¬IsMax b) :
                                  Set.Ioo a (succ b) = Set.Ioc a b
                                  theorem Order.succ_eq_succ_iff_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) (hb : ¬IsMax b) :
                                  succ a = succ b a = b
                                  theorem Order.le_succ_iff_eq_or_le {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} :
                                  a succ b a = succ b a b
                                  theorem Order.lt_succ_iff_eq_or_lt_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (hb : ¬IsMax b) :
                                  a < 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 succ b) :
                                  Set.Icc a (succ b) = insert (succ b) (Set.Icc a b)
                                  theorem Order.Ioc_succ_right {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h : a < succ b) :
                                  Set.Ioc a (succ b) = insert (succ b) (Set.Ioc a b)
                                  theorem Order.Iio_succ_eq_insert_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} (h : ¬IsMax a) :
                                  theorem Order.Ico_succ_right_eq_insert_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h₁ : a b) (h₂ : ¬IsMax b) :
                                  Set.Ico a (succ b) = insert b (Set.Ico a b)
                                  theorem Order.Ioo_succ_right_eq_insert_of_not_isMax {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h₁ : a < b) (h₂ : ¬IsMax b) :
                                  Set.Ioo a (succ b) = insert b (Set.Ioo a b)
                                  @[simp]
                                  theorem Order.lt_succ_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] :
                                  a < succ b a b
                                  theorem Order.succ_le_succ_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] :
                                  succ a succ b a b
                                  theorem Order.succ_lt_succ_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] :
                                  succ a < succ b a < b
                                  theorem Order.le_of_succ_le_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] :
                                  succ a succ ba b

                                  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 α] :
                                  succ a < 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 : α) :
                                  Set.Ico a (succ b) = Set.Icc a b
                                  @[simp]
                                  theorem Order.Ioo_succ_right {α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) :
                                  Set.Ioo a (succ b) = Set.Ioc a b
                                  @[simp]
                                  theorem Order.succ_eq_succ_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] :
                                  succ a = succ b a = b
                                  theorem Order.succ_ne_succ_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] :
                                  succ a succ b a b
                                  theorem Order.succ_ne_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] :
                                  a bsucc a succ b

                                  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 < succ b a = b a < b
                                  theorem Order.Iio_succ_eq_insert {α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a : α) :
                                  theorem Order.Ico_succ_right_eq_insert {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (h : a b) :
                                  Set.Ico a (succ b) = insert b (Set.Ico a b)
                                  theorem Order.Ioo_succ_right_eq_insert {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (h : a < b) :
                                  Set.Ioo a (succ b) = insert b (Set.Ioo a b)
                                  @[simp]
                                  theorem Order.Ioo_eq_empty_iff_le_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] :
                                  theorem Order.lt_succ_bot_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} [OrderBot α] [NoMaxOrder α] :
                                  theorem Order.le_succ_bot_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} [OrderBot α] :

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

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

                                      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.

                                      @[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 apred a < a

                                      Alias of the reverse direction of Order.pred_lt_iff_not_isMin.

                                      theorem Order.pred_wcovBy {α : Type u_1} [Preorder α] [PredOrder α] (a : α) :
                                      pred a ⩿ a
                                      theorem Order.pred_covBy_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} (h : ¬IsMin a) :
                                      pred a a
                                      theorem Order.pred_lt_of_not_isMin_of_le {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} (ha : ¬IsMin a) :
                                      a bpred a < b
                                      theorem Order.le_pred_iff_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} (ha : ¬IsMin a) :
                                      b pred a b < a
                                      theorem Order.pred_lt_pred_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} (h : a < b) (ha : ¬IsMin a) :
                                      pred a < pred b
                                      theorem Order.pred_le_pred_of_not_isMin_of_le {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} (ha : ¬IsMin a) (hb : ¬IsMin b) :
                                      a bpred a pred b
                                      @[simp]
                                      theorem Order.pred_le_pred {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} (h : a b) :
                                      theorem Order.pred_le_of_wcovBy {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} (h : a ⩿ b) :
                                      pred b a

                                      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 : α) :
                                      theorem Order.isMin_iterate_pred_of_eq_of_lt {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {n m : } (h_eq : pred^[n] a = pred^[m] a) (h_lt : n < m) :
                                      theorem Order.isMin_iterate_pred_of_eq_of_ne {α : Type u_1} [Preorder α] [PredOrder α] {a : α} {n m : } (h_eq : pred^[n] a = pred^[m] a) (h_ne : n m) :
                                      theorem Order.Ici_subset_Ioi_pred_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} (ha : ¬IsMin 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) :
                                      Set.Icc a (pred b) = Set.Ico a b
                                      theorem Order.Ioc_pred_right_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} (ha : ¬IsMin b) :
                                      Set.Ioc a (pred b) = Set.Ioo a b
                                      theorem Order.pred_lt {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) :
                                      pred a < a
                                      @[simp]
                                      theorem Order.pred_lt_of_le {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} [NoMinOrder α] :
                                      a bpred a < b
                                      @[simp]
                                      theorem Order.le_pred_iff {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} [NoMinOrder α] :
                                      a pred b a < b
                                      theorem Order.pred_le_pred_of_le {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} [NoMinOrder α] :
                                      a bpred a pred b
                                      theorem Order.pred_lt_pred {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} [NoMinOrder α] :
                                      a < bpred a < pred b
                                      theorem Order.pred_covBy {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) :
                                      pred a a
                                      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 : α) :
                                      Set.Icc a (pred b) = Set.Ico a b
                                      @[simp]
                                      theorem Order.Ioc_pred_right {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a b : α) :
                                      Set.Ioc a (pred b) = Set.Ioo a b
                                      @[simp]
                                      theorem Order.pred_eq_iff_isMin {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} :
                                      pred a = a IsMin 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.le_iff_eq_or_le_pred {α : Type u_1} [PartialOrder α] [PredOrder α] {a b : α} :
                                      a b a = b a pred b
                                      theorem Order.pred_le_le_iff {α : Type u_1} [PartialOrder α] [PredOrder α] {a b : α} :
                                      pred a b b a b = a b = pred a
                                      theorem Order.pred_eq_of_covBy {α : Type u_1} [PartialOrder α] [PredOrder α] {a b : α} (h : a b) :
                                      pred b = a

                                      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 α] :
                                      pred b = a a b
                                      @[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 α] :
                                      a pred a a =
                                      theorem Order.pred_lt_iff_ne_bot {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} [OrderBot α] :
                                      pred a < a a
                                      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 : α} :
                                      pred a < ba b
                                      theorem Order.pred_lt_iff_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} (ha : ¬IsMin a) :
                                      pred a < b a b
                                      theorem Order.pred_lt_pred_iff_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} (ha : ¬IsMin a) (hb : ¬IsMin b) :
                                      pred a < pred b a < b
                                      theorem Order.pred_le_pred_iff_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} (ha : ¬IsMin a) (hb : ¬IsMin b) :
                                      pred a pred b a 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) :
                                      Set.Ioc (pred a) b = Set.Icc a b
                                      theorem Order.Ioo_pred_left_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} (ha : ¬IsMin a) :
                                      Set.Ioo (pred a) b = Set.Ico a b
                                      theorem Order.pred_eq_pred_iff_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} (ha : ¬IsMin a) (hb : ¬IsMin b) :
                                      pred a = pred b a = b
                                      theorem Order.pred_le_iff_eq_or_le {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} :
                                      pred a b b = pred a a b
                                      theorem Order.pred_lt_iff_eq_or_lt_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} (ha : ¬IsMin a) :
                                      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.Ioi_pred_eq_insert_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} (ha : ¬IsMin a) :
                                      theorem Order.Icc_pred_left {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} (h : pred a b) :
                                      Set.Icc (pred a) b = insert (pred a) (Set.Icc a b)
                                      theorem Order.Ico_pred_left {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} (h : pred a < b) :
                                      Set.Ico (pred a) b = insert (pred a) (Set.Ico a b)
                                      @[simp]
                                      theorem Order.pred_lt_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} [NoMinOrder α] :
                                      pred a < b a b
                                      theorem Order.pred_le_pred_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} [NoMinOrder α] :
                                      pred a pred b a b
                                      theorem Order.pred_lt_pred_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} [NoMinOrder α] :
                                      pred a < pred b a < b
                                      theorem Order.le_of_pred_le_pred {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} [NoMinOrder α] :
                                      pred a pred ba b

                                      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 α] :
                                      pred a < 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 : α) :
                                      Set.Ioc (pred a) b = Set.Icc a b
                                      @[simp]
                                      theorem Order.Ioo_pred_left {α : Type u_1} [LinearOrder α] [PredOrder α] [NoMinOrder α] (a b : α) :
                                      Set.Ioo (pred a) b = Set.Ico a b
                                      @[simp]
                                      theorem Order.pred_eq_pred_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} [NoMinOrder α] :
                                      pred a = pred b a = b
                                      theorem Order.pred_ne_pred_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} [NoMinOrder α] :
                                      pred a pred b a b
                                      theorem Order.pred_ne_pred {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} [NoMinOrder α] :
                                      a bpred a pred b

                                      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 α] :
                                      pred a < b a = b a < b
                                      theorem Order.Ioi_pred_eq_insert {α : Type u_1} [LinearOrder α] [PredOrder α] [NoMinOrder α] (a : α) :
                                      theorem Order.Ico_pred_right_eq_insert {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} [NoMinOrder α] (h : a b) :
                                      Set.Ioc (pred a) b = insert a (Set.Ioc a b)
                                      theorem Order.Ioo_pred_right_eq_insert {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} [NoMinOrder α] (h : a < b) :
                                      Set.Ioo (pred a) b = insert a (Set.Ioo a b)
                                      @[simp]
                                      theorem Order.Ioo_eq_empty_iff_pred_le {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} [NoMinOrder α] :
                                      theorem Order.pred_top_lt_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} [OrderTop α] [NoMinOrder α] :
                                      theorem Order.pred_top_le_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} [OrderTop α] :

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

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

                                      Successor-predecessor orders #

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

                                      instance WithTop.instSuccOrder {α : Type u_1} [PartialOrder α] [SuccOrder α] [(a : α) → Decidable (Order.succ a = a)] :
                                      Equations
                                        @[simp]
                                        theorem WithTop.succ_coe_of_isMax {α : Type u_1} [PartialOrder α] [SuccOrder α] [(a : α) → Decidable (Order.succ a = a)] {a : α} (h : IsMax a) :
                                        theorem WithTop.succ_coe_of_not_isMax {α : Type u_1} [PartialOrder α] [SuccOrder α] [(a : α) → Decidable (Order.succ a = a)] {a : α} (h : ¬IsMax a) :
                                        Order.succ a = (Order.succ a)
                                        @[simp]
                                        theorem WithTop.succ_coe {α : Type u_1} [PartialOrder α] [SuccOrder α] [(a : α) → Decidable (Order.succ a = a)] [NoMaxOrder α] {a : α} :
                                        Order.succ a = (Order.succ a)
                                        instance WithTop.instPredOrder {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] :
                                        Equations
                                          @[simp]
                                          theorem WithTop.orderPred_top {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] :

                                          Not to be confused with WithTop.pred_bot, which is about WithTop.pred.

                                          @[simp]
                                          theorem WithTop.orderPred_coe {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] (a : α) :
                                          Order.pred a = (Order.pred a)

                                          Not to be confused with WithTop.pred_coe, which is about WithTop.pred.

                                          @[simp]
                                          theorem WithTop.pred_untop {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] (a : WithTop α) (ha : a ) :

                                          Adding a to an OrderBot #

                                          instance WithBot.instSuccOrder {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] :
                                          Equations
                                            @[simp]
                                            theorem WithBot.orderSucc_bot {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] :

                                            Not to be confused with WithBot.succ_bot, which is about WithBot.succ.

                                            @[simp]
                                            theorem WithBot.orderSucc_coe {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] (a : α) :
                                            Order.succ a = (Order.succ a)

                                            Not to be confused with WithBot.succ_coe, which is about WithBot.succ.

                                            @[simp]
                                            theorem WithBot.succ_unbot {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] (a : WithBot α) (ha : a ) :
                                            instance WithBot.instPredOrder {α : Type u_1} [PartialOrder α] [PredOrder α] [(a : α) → Decidable (Order.pred a = a)] :
                                            Equations
                                              @[simp]
                                              theorem WithBot.pred_coe_of_isMin {α : Type u_1} [PartialOrder α] [PredOrder α] [(a : α) → Decidable (Order.pred a = a)] {a : α} (h : IsMin a) :
                                              theorem WithBot.pred_coe_of_not_isMin {α : Type u_1} [PartialOrder α] [PredOrder α] [(a : α) → Decidable (Order.pred a = a)] {a : α} (h : ¬IsMin a) :
                                              Order.pred a = (Order.pred a)
                                              theorem WithBot.pred_coe {α : Type u_1} [PartialOrder α] [PredOrder α] [(a : α) → Decidable (Order.pred a = a)] [NoMinOrder α] {a : α} :
                                              Order.pred a = (Order.pred a)

                                              Adding a to a NoMinOrder #

                                              @[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
                                                        @[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_pred_notMem {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [PredOrder α] {a : s} (h : Order.pred as) :
                                                        @[deprecated isMin_of_pred_notMem (since := "2025-05-23")]
                                                        theorem isMin_of_not_pred_mem {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [PredOrder α] {a : s} (h : Order.pred as) :

                                                        Alias of isMin_of_pred_notMem.

                                                        theorem pred_notMem_iff_isMin {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [PredOrder α] [NoMinOrder α] {a : s} :
                                                        Order.pred as IsMin a
                                                        @[deprecated pred_notMem_iff_isMin (since := "2025-05-23")]
                                                        theorem not_pred_mem_iff_isMin {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [PredOrder α] [NoMinOrder α] {a : s} :
                                                        Order.pred as IsMin a

                                                        Alias of pred_notMem_iff_isMin.

                                                        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_succ_notMem {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [SuccOrder α] {a : s} (h : Order.succ as) :
                                                          @[deprecated isMax_of_succ_notMem (since := "2025-05-23")]
                                                          theorem isMax_of_not_succ_mem {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [SuccOrder α] {a : s} (h : Order.succ as) :

                                                          Alias of isMax_of_succ_notMem.

                                                          theorem succ_notMem_iff_isMax {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [SuccOrder α] [NoMaxOrder α] {a : s} :
                                                          Order.succ as IsMax a
                                                          @[deprecated succ_notMem_iff_isMax (since := "2025-05-23")]
                                                          theorem not_succ_mem_iff_isMax {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [SuccOrder α] [NoMaxOrder α] {a : s} :
                                                          Order.succ as IsMax a

                                                          Alias of succ_notMem_iff_isMax.