Successor and predecessor

This file defines successor and predecessor orders. succ a, the successor of an element a : α is the least element greater than a. pred a is the greatest element less than a. Typical examples include ℕ, ℤ, ℕ+, Fin n, but also ENat, the lexicographic order of a successor/predecessor order...

Typeclasses

• SuccOrder: Order equipped with a sensible successor function.
• PredOrder: Order equipped with a sensible predecessor function.

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 ≤ a → IsMax a

  Proof of interaction between succ and maximal element

• succ_le_of_lt {a b : α} : a < b → succ a ≤ b

  Proof that succ a is the least element greater than a

theorem SuccOrder.ext_iff {α : Type u_3} {inst✝ : Preorder α} {x y : SuccOrder α} : x = y ↔ succ = succ

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 a → IsMin a

  Proof of interaction between pred and minimal element

• le_pred_of_lt {a b : α} : a < b → a ≤ pred b

  Proof that pred b is the greatest element less than b

theorem PredOrder.ext {α : Type u_3} {inst✝ : Preorder α} {x y : PredOrder α} (pred : pred = pred) : x = y

theorem PredOrder.ext_iff {α : Type u_3} {inst✝ : Preorder α} {x y : PredOrder α} : x = y ↔ pred = pred

instance instPredOrderOrderDualOfSuccOrder {α : Type u_1} [Preorder α] [SuccOrder α] : PredOrder αᵒᵈ

instance instSuccOrderOrderDualOfPredOrder {α : Type u_1} [Preorder α] [PredOrder α] : SuccOrder αᵒᵈ

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

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

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

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

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

A constructor for SuccOrder α for α a linear order.

@[simp]

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

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

A constructor for PredOrder α for α a linear order.

@[simp]

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

noncomputable def SuccOrder.ofLinearWellFoundedLT (α : Type u_1) [LinearOrder α] [WellFoundedLT α] : SuccOrder α

A well-order is a SuccOrder.

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

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

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.

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 ≤ a → IsMax a

theorem Order.succ_le_of_lt {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} : a < b → succ a ≤ b

theorem LT.lt.succ_le {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} : a < b → Order.succ a ≤ b

Alias of Order.succ_le_of_lt.

@[simp]

theorem Order.succ_le_iff_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} : succ a ≤ a ↔ IsMax a

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

Alias of the reverse direction of Order.succ_le_iff_isMax.

theorem IsMax.of_succ_le {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} : Order.succ a ≤ a → IsMax a

Alias of the forward direction of Order.succ_le_iff_isMax.

@[simp]

theorem Order.lt_succ_iff_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} : a < succ a ↔ ¬IsMax a

theorem Order.lt_succ_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} : ¬IsMax a → a < 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) : succ a ≤ succ b

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

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) : b ≤ Order.succ a

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 ≤ succ^[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) : IsMax (succ^[n] a)

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) : IsMax (succ^[n] a)

theorem Order.Iic_subset_Iio_succ_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} (ha : ¬IsMax a) : Set.Iic a ⊆ Set.Iio (succ a)

theorem Order.Ici_succ_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a : α} (ha : ¬IsMax a) : Set.Ici (succ a) = Set.Ioi a

theorem Order.Icc_subset_Ico_succ_right_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (hb : ¬IsMax b) : Set.Icc a b ⊆ Set.Ico a (succ b)

theorem Order.Ioc_subset_Ioo_succ_right_of_not_isMax {α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (hb : ¬IsMax b) : Set.Ioc a b ⊆ Set.Ioo a (succ 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 ≤ b → a < 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.succ_strictMono {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] : StrictMono succ

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 : α) : Set.Iic a ⊆ Set.Iio (succ a)

@[simp]

theorem Order.Ici_succ {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) : Set.Ici (succ a) = Set.Ioi a

@[simp]

theorem Order.Icc_subset_Ico_succ_right {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Set.Icc a b ⊆ Set.Ico a (succ b)

@[simp]

theorem Order.Ioc_subset_Ioo_succ_right {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Set.Ioc a b ⊆ Set.Ioo a (succ 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 a → Order.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) : Order.succ 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 α] : succ ⊤ = ⊤

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 : α) : ⊥ < succ a

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

theorem Order.le_of_lt_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} : a < succ b → a ≤ 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) : Set.Iio (succ a) = Set.Iic 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 : α) : ¬IsMin (succ a)

theorem Order.Iic_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] (a : α) : Set.Iic (succ a) = insert (succ a) (Set.Iic 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) : Set.Iio (succ a) = insert a (Set.Iio 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 b → a ≤ 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 b → a < b

Alias of the forward direction of Order.succ_lt_succ_iff.

@[simp]

theorem Order.Iio_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a : α) : Set.Iio (succ a) = Set.Iic 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_injective {α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] : Function.Injective succ

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 ≠ b → succ 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 : α) : Set.Iio (succ a) = insert a (Set.Iio 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 α] : Set.Ioo a b = ∅ ↔ b ≤ succ a

theorem Order.lt_succ_bot_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} [OrderBot α] [NoMaxOrder α] : a < succ ⊥ ↔ a = ⊥

theorem Order.le_succ_bot_iff {α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} [OrderBot α] : a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥

instance Order.instSubsingletonSuccOrder {α : Type u_1} [PartialOrder α] : Subsingleton (SuccOrder α)

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

theorem Order.succ_eq_sInf {α : Type u_1} [CompleteLattice α] [SuccOrder α] (a : α) : succ a = sInf (Set.Ioi a)

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

theorem Order.succ_eq_csInf {α : Type u_1} [ConditionallyCompleteLattice α] [SuccOrder α] [NoMaxOrder α] (a : α) : succ a = sInf (Set.Ioi a)

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.

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 a → IsMin a

theorem Order.le_pred_of_lt {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} : a < b → a ≤ pred b

theorem LT.lt.le_pred {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} : a < b → a ≤ Order.pred b

Alias of Order.le_pred_of_lt.

@[simp]

theorem Order.le_pred_iff_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} : a ≤ pred a ↔ IsMin a

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

Alias of the forward direction of Order.le_pred_iff_isMin.

theorem IsMin.le_pred {α : Type u_1} [Preorder α] [PredOrder α] {a : α} : IsMin a → a ≤ 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 : α} : pred a < a ↔ ¬IsMin a

theorem Order.pred_lt_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} : ¬IsMin a → 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 : α) : 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 ≤ b → pred 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 ≤ b → pred a ≤ pred b

@[simp]

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

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

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) : Order.pred b ≤ a

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 : α) : pred^[k] x ≤ 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) : IsMin (pred^[n] a)

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) : IsMin (pred^[n] a)

theorem Order.Ici_subset_Ioi_pred_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} (ha : ¬IsMin a) : Set.Ici a ⊆ Set.Ioi (pred a)

theorem Order.Iic_pred_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a : α} (ha : ¬IsMin a) : Set.Iic (pred a) = Set.Iio a

theorem Order.Icc_subset_Ioc_pred_left_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} (ha : ¬IsMin a) : Set.Icc a b ⊆ Set.Ioc (pred a) b

theorem Order.Ico_subset_Ioo_pred_left_of_not_isMin {α : Type u_1} [Preorder α] [PredOrder α] {a b : α} (ha : ¬IsMin a) : Set.Ico a b ⊆ Set.Ioo (pred a) b

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 ≤ b → pred 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 ≤ b → pred a ≤ pred b

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

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

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 : α) : Set.Ici a ⊆ Set.Ioi (pred a)

@[simp]

theorem Order.Iic_pred {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) : Set.Iic (pred a) = Set.Iio a

@[simp]

theorem Order.Icc_subset_Ioc_pred_left {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a b : α) : Set.Icc a b ⊆ Set.Ioc (pred a) b

@[simp]

theorem Order.Ico_subset_Ioo_pred_left {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a b : α) : Set.Ico a b ⊆ Set.Ioo (pred 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 a → Order.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) : Order.pred b = a

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 α] : pred ⊥ = ⊥

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 : α) : pred a < ⊤

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

theorem Order.le_of_pred_lt {α : Type u_1} [LinearOrder α] [PredOrder α] {a b : α} : pred a < b → a ≤ 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) : Set.Ioi (pred a) = Set.Ici 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 : α) : ¬IsMax (pred a)

theorem Order.Ici_pred {α : Type u_1} [LinearOrder α] [PredOrder α] (a : α) : Set.Ici (pred a) = insert (pred a) (Set.Ici a)

theorem Order.Ioi_pred_eq_insert_of_not_isMin {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} (ha : ¬IsMin a) : Set.Ioi (pred a) = insert a (Set.Ioi 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 b → a ≤ 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 b → a < b

Alias of the forward direction of Order.pred_lt_pred_iff.

@[simp]

theorem Order.Ioi_pred {α : Type u_1} [LinearOrder α] [PredOrder α] [NoMinOrder α] (a : α) : Set.Ioi (pred a) = Set.Ici 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_injective {α : Type u_1} [LinearOrder α] [PredOrder α] [NoMinOrder α] : Function.Injective pred

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 ≠ b → pred 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 : α) : Set.Ioi (pred a) = insert a (Set.Ioi 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 α] : Set.Ioo a b = ∅ ↔ pred b ≤ a

theorem Order.pred_top_lt_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} [OrderTop α] [NoMinOrder α] : pred ⊤ < a ↔ a = ⊤

theorem Order.pred_top_le_iff {α : Type u_1} [LinearOrder α] [PredOrder α] {a : α} [OrderTop α] : pred ⊤ ≤ a ↔ a = ⊤ ∨ a = pred ⊤

instance Order.instSubsingletonPredOrder {α : Type u_1} [PartialOrder α] : Subsingleton (PredOrder α)

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

theorem Order.pred_eq_sSup {α : Type u_1} [CompleteLattice α] [PredOrder α] (a : α) : pred a = sSup (Set.Iio a)

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

theorem Order.pred_eq_csSup {α : Type u_1} [ConditionallyCompleteLattice α] [PredOrder α] [NoMinOrder α] (a : α) : pred a = sSup (Set.Iio a)

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

theorem Order.gc_pred_succ {α : Type u_1} [Preorder α] [SuccOrder α] [PredOrder α] : GaloisConnection pred succ

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

Adding a ⊤ to an OrderTop

instance WithTop.instSuccOrder {α : Type u_1} [PartialOrder α] [SuccOrder α] [(a : α) → Decidable (Order.succ a = a)] : SuccOrder (WithTop α)

@[simp]

theorem WithTop.succ_coe_of_isMax {α : Type u_1} [PartialOrder α] [SuccOrder α] [(a : α) → Decidable (Order.succ a = a)] {a : α} (h : IsMax a) : Order.succ ↑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 α] : PredOrder (WithTop α)

@[simp]

theorem WithTop.orderPred_top {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] : Order.pred ⊤ = ↑⊤

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 ≠ ⊤) : Order.pred (a.untop ha) = (Order.pred a).untop ⋯

instance WithTop.instIsEmptyPredOrderOfNonempty {α : Type u_1} [Preorder α] [NoMaxOrder α] [hα : Nonempty α] : IsEmpty (PredOrder (WithTop α))

Adding a ⊥ to an OrderBot

instance WithBot.instSuccOrder {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] : SuccOrder (WithBot α)

@[simp]

theorem WithBot.orderSucc_bot {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] : Order.succ ⊥ = ↑⊥

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 ≠ ⊥) : Order.succ (a.unbot ha) = (Order.succ a).unbot ⋯

instance WithBot.instPredOrder {α : Type u_1} [PartialOrder α] [PredOrder α] [(a : α) → Decidable (Order.pred a = a)] : PredOrder (WithBot α)

@[simp]

theorem WithBot.pred_coe_of_isMin {α : Type u_1} [PartialOrder α] [PredOrder α] [(a : α) → Decidable (Order.pred a = a)] {a : α} (h : IsMin a) : Order.pred ↑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

instance WithBot.instIsEmptySuccOrderOfNonempty {α : Type u_1} [Preorder α] [NoMinOrder α] [hα : Nonempty α] : IsEmpty (SuccOrder (WithBot α))

@[reducible, inline]

abbrev SuccOrder.ofOrderIso {X : Type u_3} {Y : Type u_4} [Preorder X] [Preorder Y] [SuccOrder X] (f : X ≃o Y) : SuccOrder Y

SuccOrder transfers across equivalences between orders.

@[reducible, inline]

abbrev PredOrder.ofOrderIso {X : Type u_3} {Y : Type u_4} [Preorder X] [Preorder Y] [PredOrder X] (f : X ≃o Y) : PredOrder Y

PredOrder transfers across equivalences between orders.

noncomputable instance Set.OrdConnected.predOrder {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [PredOrder α] : PredOrder ↑s

@[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 ↑a ∉ s) : IsMin a

@[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 ↑a ∉ s) : IsMin a

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 ↑a ∉ s ↔ 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 ↑a ∉ s ↔ IsMin a

Alias of pred_notMem_iff_isMin.

noncomputable instance Set.OrdConnected.succOrder {α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [SuccOrder α] : SuccOrder ↑s

@[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 ↑a ∉ s) : IsMax a

@[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 ↑a ∉ s) : IsMax a

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 ↑a ∉ s ↔ 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 ↑a ∉ s ↔ IsMax a

Alias of succ_notMem_iff_isMax.