Mathlib.Order.SuccPred.Basic

SuccOrder structure

(α : Type*) [Preorder α]

Full source

/-- Order equipped with a sensible successor function. -/
@[ext]
class SuccOrder (α : Type*) [Preorder α] where
  /-- Successor function -/
  succ : α → α
  /-- Proof of basic ordering with respect to `succ` -/
  le_succ : ∀ a, a ≤ succ a
  /-- Proof of interaction between `succ` and maximal element -/
  max_of_succ_le {a} : succ a ≤ a → IsMax a
  /-- Proof that `succ a` is the least element greater than `a` -/
  succ_le_of_lt {a b} : a < b → succ a ≤ b

Successor Order

Informal description

A structure defining an order equipped with a successor function `succ`, where for each element `a` in the order, `succ a` is the least element greater than `a`. This structure is sensible in that it avoids issues with maximal elements by requiring `a < succ a` for all non-maximal elements and ensuring that `succ_le_iff` and `lt_succ_iff` hold appropriately.

PredOrder structure

(α : Type*) [Preorder α]

Full source

/-- Order equipped with a sensible predecessor function. -/
@[ext]
class PredOrder (α : Type*) [Preorder α] where
  /-- Predecessor function -/
  pred : α → α
  /-- Proof of basic ordering with respect to `pred` -/
  pred_le : ∀ a, pred a ≤ a
  /-- Proof of interaction between `pred` and minimal element -/
  min_of_le_pred {a} : a ≤ pred a → IsMin a
  /-- Proof that `pred b` is the greatest element less than `b` -/
  le_pred_of_lt {a b} : a < b → a ≤ pred b

Predecessor Order

Informal description

A structure that equips a preorder $\alpha$ with a predecessor function $\mathrm{pred} : \alpha \to \alpha$, satisfying the following properties: 1. For any non-minimal element $a \in \alpha$, $\mathrm{pred} a$ is the greatest element less than $a$. 2. For any minimal element $a \in \alpha$, $\mathrm{pred} a = a$. This structure is used to define orders where every element has a sensible predecessor, such as $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{N}^+$, $\mathrm{Fin}~n$, and $\mathrm{ENat}$.

instPredOrderOrderDualOfSuccOrder instance

[Preorder α] [SuccOrder α] : PredOrder αᵒᵈ

Full source

instance [Preorder α] [SuccOrder α] :
    PredOrder αᵒᵈ where
  pred := toDualtoDual ∘ SuccOrder.succ ∘ ofDual
  pred_le := by
    simp only [comp, OrderDual.forall, ofDual_toDual, toDual_le_toDual,
     SuccOrder.le_succ, implies_true]
  min_of_le_pred h := by apply SuccOrder.max_of_succ_le h
  le_pred_of_lt := by intro a b h; exact SuccOrder.succ_le_of_lt h

Predecessor Order Structure on Order Dual of Successor Order

Informal description

For any preorder $\alpha$ equipped with a successor order structure, the order dual $\alpha^{\mathrm{op}}$ naturally inherits a predecessor order structure. Specifically, the predecessor function on $\alpha^{\mathrm{op}}$ is defined as the successor function on $\alpha$, and it satisfies the properties required for a predecessor order.

instSuccOrderOrderDualOfPredOrder instance

[Preorder α] [PredOrder α] : SuccOrder αᵒᵈ

Full source

instance [Preorder α] [PredOrder α] :
    SuccOrder αᵒᵈ where
  succ := toDualtoDual ∘ PredOrder.pred ∘ ofDual
  le_succ := by
    simp only [comp, OrderDual.forall, ofDual_toDual, toDual_le_toDual,
     PredOrder.pred_le, implies_true]
  max_of_succ_le h := by apply PredOrder.min_of_le_pred h
  succ_le_of_lt := by intro a b h; exact PredOrder.le_pred_of_lt h

Successor Order Structure on Order Dual of Predecessor Order

Informal description

For any preorder $\alpha$ equipped with a predecessor order structure, the order dual $\alpha^{\mathrm{op}}$ naturally inherits a successor order structure. Specifically, the successor function on $\alpha^{\mathrm{op}}$ is defined as the predecessor function on $\alpha$, and it satisfies the properties required for a successor order.

SuccOrder.ofSuccLeIff definition

(succ : α → α) (hsucc_le_iff : ∀ {a b}, succ a ≤ b ↔ a < b) : SuccOrder α

Full source

/-- A constructor for `SuccOrder α` usable when `α` has no maximal element. -/
def SuccOrder.ofSuccLeIff (succ : α → α) (hsucc_le_iff : ∀ {a b}, succ a ≤ b ↔ a < b) :
    SuccOrder α :=
  { succ
    le_succ := fun _ => (hsucc_le_iff.1 le_rfl).le
    max_of_succ_le := fun ha => (lt_irrefl _ <| hsucc_le_iff.1 ha).elim
    succ_le_of_lt := fun h => hsucc_le_iff.2 h }

Successor Order Construction via Order Relation

Informal description

Given a preorder $\alpha$ and a function $\mathrm{succ} : \alpha \to \alpha$, the structure `SuccOrder α` is defined when the following conditions are satisfied: 1. For any elements $a, b \in \alpha$, the inequality $\mathrm{succ} a \leq b$ holds if and only if $a < b$. 2. The function $\mathrm{succ}$ satisfies $a \leq \mathrm{succ} a$ for all $a \in \alpha$. 3. If $\mathrm{succ} a \leq a$ for some $a$, then $a$ must be a maximal element (i.e., no element is greater than $a$). 4. For any $a, b \in \alpha$, if $a < b$, then $\mathrm{succ} a \leq b$. This construction provides a way to define a successor order where $\mathrm{succ}$ correctly identifies the least element greater than any given element, and handles maximal elements appropriately.

PredOrder.ofLePredIff definition

(pred : α → α) (hle_pred_iff : ∀ {a b}, a ≤ pred b ↔ a < b) : PredOrder α

Full source

/-- A constructor for `PredOrder α` usable when `α` has no minimal element. -/
def PredOrder.ofLePredIff (pred : α → α) (hle_pred_iff : ∀ {a b}, a ≤ pred b ↔ a < b) :
    PredOrder α :=
  { pred
    pred_le := fun _ => (hle_pred_iff.1 le_rfl).le
    min_of_le_pred := fun ha => (lt_irrefl _ <| hle_pred_iff.1 ha).elim
    le_pred_of_lt := fun h => hle_pred_iff.2 h }

Predecessor Order Construction via Order Relation

Informal description

Given a preorder $\alpha$ and a function $\mathrm{pred} : \alpha \to \alpha$, the structure `PredOrder α` is defined when the following conditions are satisfied: 1. For any elements $a, b \in \alpha$, the inequality $a \leq \mathrm{pred} b$ holds if and only if $a < b$. 2. The function $\mathrm{pred}$ satisfies $\mathrm{pred} b \leq b$ for all $b \in \alpha$. 3. If $a \leq \mathrm{pred} b$ for some $a, b$, then $a$ must be a minimal element (i.e., no element is less than $a$). 4. For any $a, b \in \alpha$, if $a < b$, then $a \leq \mathrm{pred} b$. This construction provides a way to define a predecessor order where $\mathrm{pred}$ correctly identifies the greatest element less than any given element, and handles minimal elements appropriately.

SuccOrder.ofCore definition

 (succ : α → α) (hn : ∀ {a}, ¬IsMax a → ∀ b, a < b ↔ succ a ≤ b) (hm : ∀ a, IsMax a → succ a = a) : SuccOrder α

Full source

/-- A constructor for `SuccOrder α` for `α` a linear order. -/
@[simps]
def SuccOrder.ofCore (succ : α → α) (hn : ∀ {a}, ¬IsMax a → ∀ b, a < b ↔ succ a ≤ b)
    (hm : ∀ a, IsMax a → succ a = a) : SuccOrder α :=
  { succ
    succ_le_of_lt := fun {a b} =>
      by_cases (fun h hab => (hm a h).symm ▸ hab.le) fun h => (hn h b).mp
    le_succ := fun a =>
      by_cases (fun h => (hm a h).symm.le) fun h => le_of_lt <| by simpa using (hn h a).not
    max_of_succ_le := fun {a} => not_imp_not.mp fun h => by simpa using (hn h a).not }

Successor Order Construction via Core Properties

Informal description

Given a linear order $\alpha$ and a function $\mathrm{succ} : \alpha \to \alpha$, the structure `SuccOrder α` is defined when: 1. For any non-maximal element $a \in \alpha$, the inequality $a < b$ holds if and only if $\mathrm{succ} a \leq b$ for all $b \in \alpha$. 2. For any maximal element $a \in \alpha$, $\mathrm{succ} a = a$. This construction ensures that $\mathrm{succ}$ behaves as expected, providing the least element greater than $a$ for non-maximal elements and preserving maximal elements.

PredOrder.ofCore definition

 (pred : α → α) (hn : ∀ {a}, ¬IsMin a → ∀ b, b ≤ pred a ↔ b < a) (hm : ∀ a, IsMin a → pred a = a) : PredOrder α

Full source

/-- A constructor for `PredOrder α` for `α` a linear order. -/
@[simps]
def PredOrder.ofCore (pred : α → α)
    (hn : ∀ {a}, ¬IsMin a → ∀ b, b ≤ pred a ↔ b < a) (hm : ∀ a, IsMin a → pred a = a) :
    PredOrder α :=
  { pred
    le_pred_of_lt := fun {a b} =>
      by_cases (fun h hab => (hm b h).symm ▸ hab.le) fun h => (hn h a).mpr
    pred_le := fun a =>
      by_cases (fun h => (hm a h).le) fun h => le_of_lt <| by simpa using (hn h a).not
    min_of_le_pred := fun {a} => not_imp_not.mp fun h => by simpa using (hn h a).not }

Predecessor Order Construction via Core Properties

Informal description

Given a linear order $\alpha$ and a function $\mathrm{pred} : \alpha \to \alpha$, the structure `PredOrder α` is defined when: 1. For any non-minimal element $a \in \alpha$, the inequality $b \leq \mathrm{pred} a$ holds if and only if $b < a$ for all $b \in \alpha$. 2. For any minimal element $a \in \alpha$, $\mathrm{pred} a = a$. This construction ensures that $\mathrm{pred}$ behaves as expected, providing the greatest element less than $a$ for non-minimal elements and preserving minimal elements.

SuccOrder.ofLinearWellFoundedLT definition

[WellFoundedLT α] : SuccOrder α

Full source

/-- A well-order is a `SuccOrder`. -/
noncomputable def SuccOrder.ofLinearWellFoundedLT [WellFoundedLT α] : SuccOrder α :=
  ofCore (fun a ↦ if h : (Ioi a).Nonempty then wellFounded_lt.min _ h else a)
    (fun ha _ ↦ by
      rw [not_isMax_iff] at ha
      simp_rw [Set.Nonempty, mem_Ioi, dif_pos ha]
      exact ⟨(wellFounded_lt.min_le · ha), lt_of_lt_of_le (wellFounded_lt.min_mem _ ha)⟩)
    fun _ ha ↦ dif_neg (not_not_intro ha <| not_isMax_iff.mpr ·)

Successor order construction for well-founded linear orders

Informal description

Given a linear order $\alpha$ with a well-founded less-than relation, the structure `SuccOrder α` is defined where the successor function `succ` maps each non-maximal element $a$ to the minimal element in the open interval $(a, \infty)$, and leaves maximal elements unchanged. This construction ensures that for any non-maximal $a$, $a < \text{succ } a$ holds, and $\text{succ } a$ is indeed the least element greater than $a$.

PredOrder.ofLinearWellFoundedGT definition

(α) [LinearOrder α] [WellFoundedGT α] : PredOrder α

Full source

/-- A linear order with well-founded greater-than relation is a `PredOrder`. -/
noncomputable def PredOrder.ofLinearWellFoundedGT (α) [LinearOrder α] [WellFoundedGT α] :
    PredOrder α := letI := SuccOrder.ofLinearWellFoundedLT αᵒᵈ; inferInstanceAs (PredOrder αᵒᵈαᵒᵈᵒᵈ)

Predecessor order construction for well-founded linear orders

Informal description

Given a linear order $\alpha$ with a well-founded greater-than relation, the structure `PredOrder α` is defined where the predecessor function $\mathrm{pred}$ maps each non-minimal element $a$ to the greatest element less than $a$, and leaves minimal elements unchanged. This construction ensures that for any non-minimal $a$, $\mathrm{pred} a < a$ holds, and $\mathrm{pred} a$ is indeed the greatest element less than $a$.

Order.succ definition

: α → α

Full source

/-- 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`. -/
def succ : α → α :=
  SuccOrder.succ

Successor function in an ordered type

Informal description

The successor function on an ordered type $\alpha$ maps an element $a$ to the least element greater than $a$ if $a$ is not maximal, and to $a$ itself if $a$ is maximal.

Order.le_succ theorem

: ∀ a : α, a ≤ succ a

Full source

theorem le_succ : ∀ a : α, a ≤ succ a :=
  SuccOrder.le_succ

Element is Less Than or Equal to its Successor

Informal description

For any element $a$ in an ordered type $\alpha$ equipped with a successor function, the element $a$ is less than or equal to its successor, i.e., $a \leq \text{succ}(a)$.

Order.max_of_succ_le theorem

{a : α} : succ a ≤ a → IsMax a

Full source

theorem max_of_succ_le {a : α} : succ a ≤ a → IsMax a :=
  SuccOrder.max_of_succ_le

Maximality Criterion via Successor: $\text{succ}(a) \leq a$ implies $a$ is maximal

Informal description

For any element $a$ in an ordered type $\alpha$, if the successor of $a$ is less than or equal to $a$ (i.e., $\text{succ}(a) \leq a$), then $a$ is a maximal element of $\alpha$.

Order.succ_le_of_lt theorem

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

Full source

theorem succ_le_of_lt {a b : α} : a < b → succ a ≤ b :=
  SuccOrder.succ_le_of_lt

Successor Bounds Strictly Greater Elements

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, if $a < b$, then the successor of $a$ is less than or equal to $b$, i.e., $\text{succ}(a) \leq b$.

Order.succ_le_iff_isMax theorem

: succ a ≤ a ↔ IsMax a

Full source

@[simp]
theorem succ_le_iff_isMax : succsucc a ≤ a ↔ IsMax a :=
  ⟨max_of_succ_le, fun h => h <| le_succ _⟩

Maximality Criterion via Successor: $\text{succ}(a) \leq a \leftrightarrow \text{IsMax}(a)$

Informal description

For any element $a$ in an ordered type $\alpha$ equipped with a successor function, the successor of $a$ is less than or equal to $a$ if and only if $a$ is a maximal element of $\alpha$. In other words, $\text{succ}(a) \leq a \leftrightarrow \text{IsMax}(a)$.

Order.lt_succ_iff_not_isMax theorem

: a < succ a ↔ ¬IsMax a

Full source

@[simp]
theorem lt_succ_iff_not_isMax : a < succ a ↔ ¬IsMax a :=
  ⟨not_isMax_of_lt, fun ha => (le_succ a).lt_of_not_le fun h => ha <| max_of_succ_le h⟩

Characterization of Non-Maximal Elements via Successor: $a < \mathrm{succ}(a) \leftrightarrow \neg(\text{IsMax}(a))$

Informal description

For any element $a$ in an ordered type $\alpha$ equipped with a successor function, $a$ is strictly less than its successor $\mathrm{succ}(a)$ if and only if $a$ is not a maximal element of $\alpha$. In other words, $a < \mathrm{succ}(a) \leftrightarrow \neg(\text{IsMax}(a))$.

Order.wcovBy_succ theorem

(a : α) : a ⩿ succ a

Full source

theorem wcovBy_succ (a : α) : a ⩿ succ a :=
  ⟨le_succ a, fun _ hb => (succ_le_of_lt hb).not_lt⟩

Weak Covering Property of Successor: $a ⩿ \text{succ}(a)$

Informal description

For any element $a$ in an ordered type $\alpha$ equipped with a successor function, $a$ is weakly covered by its successor $\text{succ}(a)$, denoted as $a ⩿ \text{succ}(a)$. This means there is no element strictly between $a$ and $\text{succ}(a)$.

Order.covBy_succ_of_not_isMax theorem

(h : ¬IsMax a) : a ⋖ succ a

Full source

theorem covBy_succ_of_not_isMax (h : ¬IsMax a) : a ⋖ succ a :=
  (wcovBy_succ a).covBy_of_lt <| lt_succ_of_not_isMax h

Covering Property of Successor for Non-Maximal Elements: $a \lessdot \mathrm{succ}(a)$

Informal description

For any element $a$ in an ordered type $\alpha$ equipped with a successor function, if $a$ is not a maximal element, then $a$ is covered by its successor $\mathrm{succ}(a)$, denoted as $a \lessdot \mathrm{succ}(a)$. This means there is no element strictly between $a$ and $\mathrm{succ}(a)$.

Order.lt_succ_of_le_of_not_isMax theorem

(hab : b ≤ a) (ha : ¬IsMax a) : b < succ a

Full source

theorem lt_succ_of_le_of_not_isMax (hab : b ≤ a) (ha : ¬IsMax a) : b < succ a :=
  hab.trans_lt <| lt_succ_of_not_isMax ha

Strict Inequality Between Element and Successor Under Non-Maximality

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, if $b \leq a$ and $a$ is not a maximal element, then $b$ is strictly less than the successor of $a$, i.e., $b < \text{succ}(a)$.

Order.succ_le_iff_of_not_isMax theorem

(ha : ¬IsMax a) : succ a ≤ b ↔ a < b

Full source

theorem succ_le_iff_of_not_isMax (ha : ¬IsMax a) : succsucc a ≤ b ↔ a < b :=
  ⟨(lt_succ_of_not_isMax ha).trans_le, succ_le_of_lt⟩

Characterization of Successor Ordering for Non-Maximal Elements

Informal description

For any element $a$ in an ordered type $\alpha$ that is not maximal, the successor of $a$ is less than or equal to $b$ if and only if $a$ is strictly less than $b$. In other words, $\text{succ}(a) \leq b \leftrightarrow a < b$.

Order.succ_lt_succ_of_not_isMax theorem

(h : a < b) (hb : ¬IsMax b) : succ a < succ b

Full source

lemma succ_lt_succ_of_not_isMax (h : a < b) (hb : ¬ IsMax b) : succ a < succ b :=
  lt_succ_of_le_of_not_isMax (succ_le_of_lt h) hb

Strict Monotonicity of Successor Function for Non-Maximal Elements

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, if $a < b$ and $b$ is not a maximal element, then the successor of $a$ is strictly less than the successor of $b$, i.e., $\text{succ}(a) < \text{succ}(b)$.

Order.succ_le_succ theorem

(h : a ≤ b) : succ a ≤ succ b

Full source

@[simp, mono, gcongr]
theorem succ_le_succ (h : a ≤ b) : succ a ≤ succ b := by
  by_cases hb : IsMax b
  · by_cases hba : b ≤ a
    · exact (hb <| hba.trans <| le_succ _).trans (le_succ _)
    · exact succ_le_of_lt ((h.lt_of_not_le hba).trans_le <| le_succ b)
  · rw [succ_le_iff_of_not_isMax fun ha => hb <| ha.mono h]
    apply lt_succ_of_le_of_not_isMax h hb

Monotonicity of the Successor Function

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, if $a \leq b$, then the successor of $a$ is less than or equal to the successor of $b$, i.e., $\text{succ}(a) \leq \text{succ}(b)$.

Order.succ_mono theorem

: Monotone (succ : α → α)

Full source

theorem succ_mono : Monotone (succ : α → α) := fun _ _ => succ_le_succ

Monotonicity of the Successor Function

Informal description

The successor function $\text{succ} : \alpha \to \alpha$ is monotone, meaning that for any elements $a, b \in \alpha$, if $a \leq b$, then $\text{succ}(a) \leq \text{succ}(b)$.

Order.le_succ_of_wcovBy theorem

(h : a ⩿ b) : b ≤ succ a

Full source

/-- See also `Order.succ_eq_of_covBy`. -/
lemma le_succ_of_wcovBy (h : a ⩿ b) : b ≤ succ a := by
  obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le
  · by_contra hba
    exact h.2 (lt_succ_of_not_isMax hab.lt.not_isMax) <| hab.lt.succ_le.lt_of_not_le hba
  · exact hba.trans (le_succ _)

Weak Covering Implies Successor Bound

Informal description

For any two elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, if $a$ is weakly covered by $b$ (denoted $a ⩿ b$), then $b$ is less than or equal to the successor of $a$, i.e., $b \leq \text{succ}(a)$.

Order.le_succ_iterate theorem

(k : ℕ) (x : α) : x ≤ succ^[k] x

Full source

theorem le_succ_iterate (k : ℕ) (x : α) : x ≤ succsucc^[k] x :=
  id_le_iterate_of_id_le le_succ _ _

Monotonicity of Successor Iterates

Informal description

For any natural number $k$ and any element $x$ in an ordered type $\alpha$ equipped with a successor function, the $k$-th iterate of the successor function applied to $x$ is greater than or equal to $x$, i.e., $x \leq \text{succ}^k(x)$.

Order.isMax_iterate_succ_of_eq_of_lt theorem

{n m : ℕ} (h_eq : succ^[n] a = succ^[m] a) (h_lt : n < m) : IsMax (succ^[n] a)

Full source

theorem isMax_iterate_succ_of_eq_of_lt {n m : ℕ} (h_eq : succsucc^[n] a = succsucc^[m] a)
    (h_lt : n < m) : IsMax (succsucc^[n] a) := by
  refine max_of_succ_le (le_trans ?_ h_eq.symm.le)
  rw [← iterate_succ_apply' succ]
  have h_le : n + 1 ≤ m := Nat.succ_le_of_lt h_lt
  exact Monotone.monotone_iterate_of_le_map succ_mono (le_succ a) h_le

Maximality of Iterated Successor at Equal Points with $n < m$

Informal description

For any natural numbers $n$ and $m$ and any element $a$ in an ordered type $\alpha$ with a successor function, if the $n$-th iterate of the successor function applied to $a$ equals the $m$-th iterate (i.e., $\text{succ}^n(a) = \text{succ}^m(a)$) and $n < m$, then the element $\text{succ}^n(a)$ is maximal in $\alpha$.

Order.isMax_iterate_succ_of_eq_of_ne theorem

{n m : ℕ} (h_eq : succ^[n] a = succ^[m] a) (h_ne : n ≠ m) : IsMax (succ^[n] a)

Full source

theorem isMax_iterate_succ_of_eq_of_ne {n m : ℕ} (h_eq : succsucc^[n] a = succsucc^[m] a)
    (h_ne : n ≠ m) : IsMax (succsucc^[n] a) := by
  rcases le_total n m with h | h
  · exact isMax_iterate_succ_of_eq_of_lt h_eq (lt_of_le_of_ne h h_ne)
  · rw [h_eq]
    exact isMax_iterate_succ_of_eq_of_lt h_eq.symm (lt_of_le_of_ne h h_ne.symm)

Maximality of Iterated Successor at Equal Points with $n \neq m$

Informal description

For any natural numbers $n$ and $m$ and any element $a$ in an ordered type $\alpha$ with a successor function, if the $n$-th iterate of the successor function applied to $a$ equals the $m$-th iterate (i.e., $\text{succ}^n(a) = \text{succ}^m(a)$) and $n \neq m$, then the element $\text{succ}^n(a)$ is maximal in $\alpha$.

Order.Iic_subset_Iio_succ_of_not_isMax theorem

(ha : ¬IsMax a) : Iic a ⊆ Iio (succ a)

Full source

theorem Iic_subset_Iio_succ_of_not_isMax (ha : ¬IsMax a) : IicIic a ⊆ Iio (succ a) :=
  fun _ => (lt_succ_of_le_of_not_isMax · ha)

Inclusion of Closed Interval in Open Successor Interval for Non-Maximal Elements

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a successor function, if $a$ is not a maximal element, then the left-infinite right-closed interval $(-\infty, a]$ is contained in the left-infinite right-open interval $(-\infty, \text{succ}(a))$.

Order.Ici_succ_of_not_isMax theorem

(ha : ¬IsMax a) : Ici (succ a) = Ioi a

Full source

theorem Ici_succ_of_not_isMax (ha : ¬IsMax a) : Ici (succ a) = Ioi a :=
  Set.ext fun _ => succ_le_iff_of_not_isMax ha

Successor Interval Equality for Non-Maximal Elements: $[\text{succ}(a), \infty) = (a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$ that is not maximal, the left-closed right-infinite interval starting at the successor of $a$ is equal to the left-open right-infinite interval starting at $a$. In other words, $[\text{succ}(a), \infty) = (a, \infty)$.

Order.Icc_subset_Ico_succ_right_of_not_isMax theorem

(hb : ¬IsMax b) : Icc a b ⊆ Ico a (succ b)

Full source

theorem Icc_subset_Ico_succ_right_of_not_isMax (hb : ¬IsMax b) : IccIcc a b ⊆ Ico a (succ b) := by
  rw [← Ici_inter_Iio, ← Ici_inter_Iic]
  gcongr
  intro _ h
  apply lt_succ_of_le_of_not_isMax h hb

Inclusion of Closed Interval in Left-Closed Right-Open Interval Under Successor for Non-Maximal Elements

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if $b$ is not a maximal element, then the closed interval $[a, b]$ is contained in the left-closed right-open interval $[a, \text{succ}(b))$. In symbols: $$ [a, b] \subseteq [a, \text{succ}(b)). $$

Order.Ioc_subset_Ioo_succ_right_of_not_isMax theorem

(hb : ¬IsMax b) : Ioc a b ⊆ Ioo a (succ b)

Full source

theorem Ioc_subset_Ioo_succ_right_of_not_isMax (hb : ¬IsMax b) : IocIoc a b ⊆ Ioo a (succ b) := by
  rw [← Ioi_inter_Iio, ← Ioi_inter_Iic]
  gcongr
  intro _ h
  apply Iic_subset_Iio_succ_of_not_isMax hb h

Inclusion of $(a, b]$ in $(a, \text{succ}(b))$ for non-maximal $b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if $b$ is not a maximal element, then the left-open right-closed interval $(a, b]$ is contained in the left-open right-open interval $(a, \text{succ}(b))$. In symbols: $$ (a, b] \subseteq (a, \text{succ}(b)). $$

Order.Icc_succ_left_of_not_isMax theorem

(ha : ¬IsMax a) : Icc (succ a) b = Ioc a b

Full source

theorem Icc_succ_left_of_not_isMax (ha : ¬IsMax a) : Icc (succ a) b = Ioc a b := by
  rw [← Ici_inter_Iic, Ici_succ_of_not_isMax ha, Ioi_inter_Iic]

Successor Interval Equality: $[\text{succ}(a), b] = (a, b]$ for Non-Maximal $a$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if $a$ is not a maximal element, then the closed interval $[\text{succ}(a), b]$ is equal to the left-open right-closed interval $(a, b]$. In symbols: $$ [\text{succ}(a), b] = (a, b]. $$

Order.Ico_succ_left_of_not_isMax theorem

(ha : ¬IsMax a) : Ico (succ a) b = Ioo a b

Full source

theorem Ico_succ_left_of_not_isMax (ha : ¬IsMax a) : Ico (succ a) b = Ioo a b := by
  rw [← Ici_inter_Iio, Ici_succ_of_not_isMax ha, Ioi_inter_Iio]

Successor Interval Equality: $[\text{succ}(a), b) = (a, b)$ for non-maximal $a$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, if $a$ is not a maximal element, then the left-closed right-open interval $[\text{succ}(a), b)$ is equal to the open interval $(a, b)$. In other words: $$ [\text{succ}(a), b) = (a, b) $$

Order.lt_succ theorem

(a : α) : a < succ a

Full source

theorem lt_succ (a : α) : a < succ a :=
  lt_succ_of_not_isMax <| not_isMax a

Element is Less Than Its Successor

Informal description

For any element $a$ in an ordered type $\alpha$ equipped with a successor function, $a$ is strictly less than its successor, i.e., $a < \text{succ}(a)$.

Order.lt_succ_of_le theorem

: a ≤ b → a < succ b

Full source

@[simp]
theorem lt_succ_of_le : a ≤ b → a < succ b :=
  (lt_succ_of_le_of_not_isMax · <| not_isMax b)

Element is Less Than Successor of Greater or Equal Element

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, if $a \leq b$, then $a$ is strictly less than the successor of $b$, i.e., $a < \text{succ}(b)$.

Order.succ_le_iff theorem

: succ a ≤ b ↔ a < b

Full source

@[simp]
theorem succ_le_iff : succsucc a ≤ b ↔ a < b :=
  succ_le_iff_of_not_isMax <| not_isMax a

Characterization of Successor Ordering: $\text{succ}(a) \leq b \leftrightarrow a < b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, the successor of $a$ is less than or equal to $b$ if and only if $a$ is strictly less than $b$. In other words, $\text{succ}(a) \leq b \leftrightarrow a < b$.

Order.succ_lt_succ theorem

(hab : a < b) : succ a < succ b

Full source

@[gcongr] theorem succ_lt_succ (hab : a < b) : succ a < succ b := by simp [hab]

Strict Monotonicity of Successor Function: $a < b \Rightarrow \text{succ}(a) < \text{succ}(b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if $a < b$, then the successor of $a$ is strictly less than the successor of $b$.

Order.succ_strictMono theorem

: StrictMono (succ : α → α)

Full source

theorem succ_strictMono : StrictMono (succ : α → α) := fun _ _ => succ_lt_succ

Strict Monotonicity of the Successor Function

Informal description

The successor function $\text{succ} : \alpha \to \alpha$ is strictly monotone, meaning that for any elements $a, b \in \alpha$, if $a < b$, then $\text{succ}(a) < \text{succ}(b)$.

Order.covBy_succ theorem

(a : α) : a ⋖ succ a

Full source

theorem covBy_succ (a : α) : a ⋖ succ a :=
  covBy_succ_of_not_isMax <| not_isMax a

Covering Property of Successor Function: $a \lessdot \mathrm{succ}(a)$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a successor function, $a$ is covered by its successor $\mathrm{succ}(a)$, denoted as $a \lessdot \mathrm{succ}(a)$. This means there is no element strictly between $a$ and $\mathrm{succ}(a)$.

Order.Iic_subset_Iio_succ theorem

(a : α) : Iic a ⊆ Iio (succ a)

Full source

theorem Iic_subset_Iio_succ (a : α) : IicIic a ⊆ Iio (succ a) := by simp

Inclusion of Closed Interval in Open Successor Interval

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a successor function, the left-infinite right-closed interval $(-\infty, a]$ is contained in the left-infinite right-open interval $(-\infty, \text{succ}(a))$. In other words, if $x \leq a$, then $x < \text{succ}(a)$.

Order.Ici_succ theorem

(a : α) : Ici (succ a) = Ioi a

Full source

@[simp]
theorem Ici_succ (a : α) : Ici (succ a) = Ioi a :=
  Ici_succ_of_not_isMax <| not_isMax _

Successor Interval Equality: $[\mathrm{succ}(a), \infty) = (a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a successor function, the left-closed right-infinite interval starting at the successor of $a$ is equal to the left-open right-infinite interval starting at $a$, i.e., $[\mathrm{succ}(a), \infty) = (a, \infty)$.

Order.Icc_subset_Ico_succ_right theorem

(a b : α) : Icc a b ⊆ Ico a (succ b)

Full source

@[simp]
theorem Icc_subset_Ico_succ_right (a b : α) : IccIcc a b ⊆ Ico a (succ b) :=
  Icc_subset_Ico_succ_right_of_not_isMax <| not_isMax _

Inclusion of Closed Interval in Left-Closed Right-Open Interval Under Successor

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, the closed interval $[a, b]$ is contained in the left-closed right-open interval $[a, \text{succ}(b))$. In symbols: $$ [a, b] \subseteq [a, \text{succ}(b)). $$

Order.Ioc_subset_Ioo_succ_right theorem

(a b : α) : Ioc a b ⊆ Ioo a (succ b)

Full source

@[simp]
theorem Ioc_subset_Ioo_succ_right (a b : α) : IocIoc a b ⊆ Ioo a (succ b) :=
  Ioc_subset_Ioo_succ_right_of_not_isMax <| not_isMax _

Inclusion of $(a, b]$ in $(a, \text{succ}(b))$ under successor operation

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, the left-open right-closed interval $(a, b]$ is contained in the left-open right-open interval $(a, \text{succ}(b))$. In symbols: $$ (a, b] \subseteq (a, \text{succ}(b)). $$

Order.Icc_succ_left theorem

(a b : α) : Icc (succ a) b = Ioc a b

Full source

@[simp]
theorem Icc_succ_left (a b : α) : Icc (succ a) b = Ioc a b :=
  Icc_succ_left_of_not_isMax <| not_isMax _

Equality of Closed Interval and Left-Open Right-Closed Interval under Successor

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, the closed interval $[\text{succ}(a), b]$ is equal to the left-open right-closed interval $(a, b]$. In symbols: $$ [\text{succ}(a), b] = (a, b]. $$

Order.Ico_succ_left theorem

(a b : α) : Ico (succ a) b = Ioo a b

Full source

@[simp]
theorem Ico_succ_left (a b : α) : Ico (succ a) b = Ioo a b :=
  Ico_succ_left_of_not_isMax <| not_isMax _

Successor Interval Equality: $[\text{succ}(a), b) = (a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, the left-closed right-open interval $[\text{succ}(a), b)$ is equal to the open interval $(a, b)$. In other words: $$ [\text{succ}(a), b) = (a, b) $$

Order.succ_eq_iff_isMax theorem

: succ a = a ↔ IsMax a

Full source

@[simp]
theorem succ_eq_iff_isMax : succsucc a = a ↔ IsMax a :=
  ⟨fun h => max_of_succ_le h.le, fun h => h.eq_of_ge <| le_succ _⟩

Successor Equals Self iff Maximal

Informal description

For any element $a$ in an ordered type $\alpha$ equipped with a successor function, the successor of $a$ equals $a$ if and only if $a$ is a maximal element of $\alpha$. In other words, $\text{succ}(a) = a \leftrightarrow \text{IsMax}(a)$.

Order.le_iff_eq_or_succ_le theorem

: a ≤ b ↔ a = b ∨ succ a ≤ b

Full source

lemma le_iff_eq_or_succ_le : a ≤ b ↔ a = b ∨ succ a ≤ b := by
  by_cases ha : IsMax a
  · simpa [ha.succ_eq] using le_of_eq
  · rw [succ_le_iff_of_not_isMax ha, le_iff_eq_or_lt]

Characterization of Ordering via Successor: $a \leq b \leftrightarrow (a = b \lor \text{succ}(a) \leq b)$

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, $a \leq b$ if and only if either $a = b$ or the successor of $a$ is less than or equal to $b$. In other words: $$ a \leq b \leftrightarrow (a = b \lor \text{succ}(a) \leq b) $$

Order.le_le_succ_iff theorem

: a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a

Full source

theorem le_le_succ_iff : a ≤ b ∧ b ≤ succ aa ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a := by
  refine
    ⟨fun h =>
      or_iff_not_imp_left.2 fun hba : b ≠ a =>
        h.2.antisymm (succ_le_of_lt <| h.1.lt_of_ne <| hba.symm),
      ?_⟩
  rintro (rfl | rfl)
  · exact ⟨le_rfl, le_succ b⟩
  · exact ⟨le_succ a, le_rfl⟩

Characterization of Elements Between $a$ and $\text{succ}(a)$

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, the conjunction $a \leq b \land b \leq \text{succ}(a)$ holds if and only if $b$ is equal to either $a$ or its successor $\text{succ}(a)$.

Order.succ_eq_of_covBy theorem

(h : a ⋖ b) : succ a = b

Full source

/-- See also `Order.le_succ_of_wcovBy`. -/
lemma succ_eq_of_covBy (h : a ⋖ b) : succ a = b := (succ_le_of_lt h.lt).antisymm h.wcovBy.le_succ

Successor of Covered Element: $\text{succ}(a) = b$ when $a \lessdot b$

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, if $a$ is covered by $b$ (denoted $a \lessdot b$), then the successor of $a$ equals $b$, i.e., $\text{succ}(a) = b$.

OrderIso.map_succ theorem

[PartialOrder β] [SuccOrder β] (f : α ≃o β) (a : α) : f (succ a) = succ (f a)

Full source

theorem _root_.OrderIso.map_succ [PartialOrder β] [SuccOrder β] (f : α ≃o β) (a : α) :
    f (succ a) = succ (f a) := by
  by_cases h : IsMax a
  · rw [h.succ_eq, (f.isMax_apply.2 h).succ_eq]
  · exact (f.map_covBy.2 <| covBy_succ_of_not_isMax h).succ_eq.symm

Order Isomorphism Preserves Successor: $f(\mathrm{succ}(a)) = \mathrm{succ}(f(a))$

Informal description

Let $\alpha$ and $\beta$ be partially ordered sets equipped with successor functions, and let $f : \alpha \simeq \beta$ be an order isomorphism. Then for any element $a \in \alpha$, the image of the successor of $a$ under $f$ equals the successor of the image of $a$ under $f$, i.e., $f(\mathrm{succ}(a)) = \mathrm{succ}(f(a))$.

Order.succ_eq_iff_covBy theorem

: succ a = b ↔ a ⋖ b

Full source

theorem succ_eq_iff_covBy : succsucc a = b ↔ a ⋖ b :=
  ⟨by rintro rfl; exact covBy_succ _, CovBy.succ_eq⟩

Successor Equals $b$ if and only if $a$ is Covered by $b$

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, the successor of $a$ equals $b$ if and only if $a$ is covered by $b$ (i.e., there is no element strictly between $a$ and $b$). In symbols: $$\text{succ}(a) = b \leftrightarrow a \lessdot b.$$

Order.succ_top theorem

: succ (⊤ : α) = ⊤

Full source

@[simp]
theorem succ_top : succ (⊤ : α) = ⊤ := by
  rw [succ_eq_iff_isMax, isMax_iff_eq_top]

Successor of Top Element is Top

Informal description

In an ordered type $\alpha$ with a greatest element $\top$ and a successor function $\text{succ}$, the successor of $\top$ is $\top$ itself, i.e., $\text{succ}(\top) = \top$.

Order.succ_le_iff_eq_top theorem

: succ a ≤ a ↔ a = ⊤

Full source

theorem succ_le_iff_eq_top : succsucc a ≤ a ↔ a = ⊤ :=
  succ_le_iff_isMax.trans isMax_iff_eq_top

Maximality Criterion via Successor: $\text{succ}(a) \leq a \leftrightarrow a = \top$

Informal description

For any element $a$ in an ordered type $\alpha$ with a greatest element $\top$, the successor of $a$ is less than or equal to $a$ if and only if $a$ equals $\top$. In other words, $\text{succ}(a) \leq a \leftrightarrow a = \top$.

Order.lt_succ_iff_ne_top theorem

: a < succ a ↔ a ≠ ⊤

Full source

theorem lt_succ_iff_ne_top : a < succ a ↔ a ≠ ⊤ :=
  lt_succ_iff_not_isMax.trans not_isMax_iff_ne_top

Characterization of Non-Top Elements via Successor: $a < \mathrm{succ}(a) \leftrightarrow a \neq \top$

Informal description

For any element $a$ in an ordered type $\alpha$ with a greatest element $\top$, the element $a$ is strictly less than its successor $\mathrm{succ}(a)$ if and only if $a$ is not equal to $\top$, i.e., $a < \mathrm{succ}(a) \leftrightarrow a \neq \top$.

Order.bot_lt_succ theorem

(a : α) : ⊥ < succ a

Full source

theorem bot_lt_succ (a : α) : ⊥ < succ a :=
  (lt_succ_of_not_isMax not_isMax_bot).trans_le <| succ_mono bot_le

Bottom Element is Strictly Below Successor

Informal description

For any element $a$ in an ordered type $\alpha$ with a bottom element $\bot$ and a successor function $\mathrm{succ}$, the bottom element is strictly less than the successor of $a$, i.e., $\bot < \mathrm{succ}(a)$.

Order.succ_ne_bot theorem

(a : α) : succ a ≠ ⊥

Full source

theorem succ_ne_bot (a : α) : succsucc a ≠ ⊥ :=
  (bot_lt_succ a).ne'

Successor Never Equals Bottom Element

Informal description

For any element $a$ in an ordered type $\alpha$ with a bottom element $\bot$ and a successor function $\mathrm{succ}$, the successor of $a$ is not equal to the bottom element, i.e., $\mathrm{succ}(a) \neq \bot$.

Order.le_of_lt_succ theorem

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

Full source

theorem le_of_lt_succ {a b : α} : a < succ b → a ≤ b := fun h ↦ by
  by_contra! nh
  exact (h.trans_le (succ_le_of_lt nh)).false

Strictly Below Successor Implies Non-Strictly Below

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, if $a$ is strictly less than the successor of $b$, then $a$ is less than or equal to $b$, i.e., $a \leq b$.

Order.lt_succ_iff_of_not_isMax theorem

(ha : ¬IsMax a) : b < succ a ↔ b ≤ a

Full source

theorem lt_succ_iff_of_not_isMax (ha : ¬IsMax a) : b < succ a ↔ b ≤ a :=
  ⟨le_of_lt_succ, fun h => h.trans_lt <| lt_succ_of_not_isMax ha⟩

Characterization of Strictly Below Successor for Non-Maximal Elements

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a successor function, if $a$ is not maximal, then for any element $b$, $b$ is strictly less than the successor of $a$ if and only if $b$ is less than or equal to $a$. In symbols: $$ b < \text{succ}(a) \leftrightarrow b \leq a $$

Order.succ_lt_succ_iff_of_not_isMax theorem

(ha : ¬IsMax a) (hb : ¬IsMax b) : succ a < succ b ↔ a < b

Full source

theorem succ_lt_succ_iff_of_not_isMax (ha : ¬IsMax a) (hb : ¬IsMax b) :
    succsucc a < succ b ↔ a < b := by
  rw [lt_succ_iff_of_not_isMax hb, succ_le_iff_of_not_isMax ha]

Strict Monotonicity of Successor Function for Non-Maximal Elements

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if neither $a$ nor $b$ is maximal, then the successor of $a$ is strictly less than the successor of $b$ if and only if $a$ is strictly less than $b$. In symbols: $$\text{succ}(a) < \text{succ}(b) \leftrightarrow a < b$$

Order.succ_le_succ_iff_of_not_isMax theorem

(ha : ¬IsMax a) (hb : ¬IsMax b) : succ a ≤ succ b ↔ a ≤ b

Full source

theorem succ_le_succ_iff_of_not_isMax (ha : ¬IsMax a) (hb : ¬IsMax b) :
    succsucc a ≤ succ b ↔ a ≤ b := by
  rw [succ_le_iff_of_not_isMax ha, lt_succ_iff_of_not_isMax hb]

Monotonicity of Successor Function for Non-Maximal Elements

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if neither $a$ nor $b$ is maximal, then the successor of $a$ is less than or equal to the successor of $b$ if and only if $a$ is less than or equal to $b$. In symbols: $$ \text{succ}(a) \leq \text{succ}(b) \leftrightarrow a \leq b $$

Order.Iio_succ_of_not_isMax theorem

(ha : ¬IsMax a) : Iio (succ a) = Iic a

Full source

theorem Iio_succ_of_not_isMax (ha : ¬IsMax a) : Iio (succ a) = Iic a :=
  Set.ext fun _ => lt_succ_iff_of_not_isMax ha

Equality of Intervals for Non-Maximal Elements: $(-\infty, \text{succ}(a)) = (-\infty, a]$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a successor function, if $a$ is not maximal, then the left-infinite right-open interval $(-\infty, \text{succ}(a))$ is equal to the left-infinite right-closed interval $(-\infty, a]$. In symbols: $$ (-\infty, \text{succ}(a)) = (-\infty, a] $$

Order.Ico_succ_right_of_not_isMax theorem

(hb : ¬IsMax b) : Ico a (succ b) = Icc a b

Full source

theorem Ico_succ_right_of_not_isMax (hb : ¬IsMax b) : Ico a (succ b) = Icc a b := by
  rw [← Ici_inter_Iio, Iio_succ_of_not_isMax hb, Ici_inter_Iic]

Interval Equality for Non-Maximal Elements: $[a, \text{succ}(b)) = [a, b]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if $b$ is not maximal, then the left-closed right-open interval $[a, \text{succ}(b))$ is equal to the closed interval $[a, b]$. In symbols: $$ [a, \text{succ}(b)) = [a, b] $$

Order.Ioo_succ_right_of_not_isMax theorem

(hb : ¬IsMax b) : Ioo a (succ b) = Ioc a b

Full source

theorem Ioo_succ_right_of_not_isMax (hb : ¬IsMax b) : Ioo a (succ b) = Ioc a b := by
  rw [← Ioi_inter_Iio, Iio_succ_of_not_isMax hb, Ioi_inter_Iic]

Open Interval Equals Left-Open Right-Closed Interval for Non-Maximal Elements

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if $b$ is not maximal, then the open interval $(a, \text{succ}(b))$ is equal to the left-open right-closed interval $(a, b]$. In symbols: $$ (a, \text{succ}(b)) = (a, b] $$

Order.succ_eq_succ_iff_of_not_isMax theorem

(ha : ¬IsMax a) (hb : ¬IsMax b) : succ a = succ b ↔ a = b

Full source

theorem succ_eq_succ_iff_of_not_isMax (ha : ¬IsMax a) (hb : ¬IsMax b) :
    succsucc a = succ b ↔ a = b := by
  rw [eq_iff_le_not_lt, eq_iff_le_not_lt, succ_le_succ_iff_of_not_isMax ha hb,
    succ_lt_succ_iff_of_not_isMax ha hb]

Injectivity of Successor Function for Non-Maximal Elements

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if neither $a$ nor $b$ is maximal, then the successor of $a$ equals the successor of $b$ if and only if $a$ equals $b$. In symbols: $$ \text{succ}(a) = \text{succ}(b) \leftrightarrow a = b $$

Order.le_succ_iff_eq_or_le theorem

: a ≤ succ b ↔ a = succ b ∨ a ≤ b

Full source

theorem le_succ_iff_eq_or_le : a ≤ succ b ↔ a = succ b ∨ a ≤ b := by
  by_cases hb : IsMax b
  · rw [hb.succ_eq, or_iff_right_of_imp le_of_eq]
  · rw [← lt_succ_iff_of_not_isMax hb, le_iff_eq_or_lt]

Characterization of Elements Below Successor

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, $a$ is less than or equal to the successor of $b$ if and only if either $a$ equals the successor of $b$ or $a$ is less than or equal to $b$. In symbols: $$ a \leq \text{succ}(b) \leftrightarrow a = \text{succ}(b) \lor a \leq b $$

Order.lt_succ_iff_eq_or_lt_of_not_isMax theorem

(hb : ¬IsMax b) : a < succ b ↔ a = b ∨ a < b

Full source

theorem lt_succ_iff_eq_or_lt_of_not_isMax (hb : ¬IsMax b) : a < succ b ↔ a = b ∨ a < b :=
  (lt_succ_iff_of_not_isMax hb).trans le_iff_eq_or_lt

Characterization of Strictly Below Successor for Non-Maximal Elements

Informal description

For any element $b$ in a preorder $\alpha$ equipped with a successor function, if $b$ is not maximal, then for any element $a$, the inequality $a < \text{succ}(b)$ holds if and only if either $a = b$ or $a < b$. In symbols: $$ a < \text{succ}(b) \leftrightarrow (a = b \lor a < b) $$

Order.not_isMin_succ theorem

[Nontrivial α] (a : α) : ¬IsMin (succ a)

Full source

theorem not_isMin_succ [Nontrivial α] (a : α) : ¬ IsMin (succ a) := by
  obtain ha | ha := (le_succ a).eq_or_lt
  · exact (ha ▸ succ_eq_iff_isMax.1 ha.symm).not_isMin
  · exact not_isMin_of_lt ha

Successor is Not Minimal in Nontrivial Order

Informal description

In a nontrivial ordered type $\alpha$ equipped with a successor function, the successor of any element $a$ is not a minimal element. That is, $\neg \text{IsMin}(\text{succ}(a))$ for all $a \in \alpha$.

Order.Iic_succ theorem

(a : α) : Iic (succ a) = insert (succ a) (Iic a)

Full source

theorem Iic_succ (a : α) : Iic (succ a) = insert (succ a) (Iic a) :=
  ext fun _ => le_succ_iff_eq_or_le

Decomposition of Interval Below Successor

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a successor function, the left-infinite right-closed interval $(-\infty, \text{succ}(a)]$ is equal to the union of the singleton set $\{\text{succ}(a)\}$ and the interval $(-\infty, a]$. In symbols: $$ (-\infty, \text{succ}(a)] = \{\text{succ}(a)\} \cup (-\infty, a] $$

Order.Icc_succ_right theorem

(h : a ≤ succ b) : Icc a (succ b) = insert (succ b) (Icc a b)

Full source

theorem Icc_succ_right (h : a ≤ succ b) : Icc a (succ b) = insert (succ b) (Icc a b) := by
  simp_rw [← Ici_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ici.2 h)]

Decomposition of Closed Interval at Successor

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if $a \leq \text{succ}(b)$, then the closed interval $[a, \text{succ}(b)]$ is equal to the union of the singleton set $\{\text{succ}(b)\}$ and the closed interval $[a, b]$. In symbols: $$ [a, \text{succ}(b)] = \{\text{succ}(b)\} \cup [a, b] $$

Order.Ioc_succ_right theorem

(h : a < succ b) : Ioc a (succ b) = insert (succ b) (Ioc a b)

Full source

theorem Ioc_succ_right (h : a < succ b) : Ioc a (succ b) = insert (succ b) (Ioc a b) := by
  simp_rw [← Ioi_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ioi.2 h)]

Decomposition of Left-Open Right-Closed Interval at Successor

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if $a < \text{succ}(b)$, then the left-open right-closed interval $(a, \text{succ}(b)]$ is equal to the union of the singleton set $\{\text{succ}(b)\}$ and the interval $(a, b]$. In symbols: $$ (a, \text{succ}(b)] = \{\text{succ}(b)\} \cup (a, b] $$

Order.Iio_succ_eq_insert_of_not_isMax theorem

(h : ¬IsMax a) : Iio (succ a) = insert a (Iio a)

Full source

theorem Iio_succ_eq_insert_of_not_isMax (h : ¬IsMax a) : Iio (succ a) = insert a (Iio a) :=
  ext fun _ => lt_succ_iff_eq_or_lt_of_not_isMax h

Interval Characterization for Successor of Non-Maximal Element

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a successor function, if $a$ is not maximal, then the left-infinite right-open interval $(-\infty, \text{succ}(a))$ is equal to the union of $\{a\}$ and the interval $(-\infty, a)$. In symbols: $$ (-\infty, \text{succ}(a)) = \{a\} \cup (-\infty, a) $$

Order.Ico_succ_right_eq_insert_of_not_isMax theorem

(h₁ : a ≤ b) (h₂ : ¬IsMax b) : Ico a (succ b) = insert b (Ico a b)

Full source

theorem Ico_succ_right_eq_insert_of_not_isMax (h₁ : a ≤ b) (h₂ : ¬IsMax b) :
    Ico a (succ b) = insert b (Ico a b) := by
  simp_rw [← Iio_inter_Ici, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ici.2 h₁)]

Interval Decomposition for Successor of Non-Maximal Element: $[a, \text{succ}(b)) = \{b\} \cup [a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if $a \leq b$ and $b$ is not a maximal element, then the left-closed right-open interval $[a, \text{succ}(b))$ is equal to the union of $\{b\}$ and the interval $[a, b)$. In symbols: $$ [a, \text{succ}(b)) = \{b\} \cup [a, b) $$

Order.Ioo_succ_right_eq_insert_of_not_isMax theorem

(h₁ : a < b) (h₂ : ¬IsMax b) : Ioo a (succ b) = insert b (Ioo a b)

Full source

theorem Ioo_succ_right_eq_insert_of_not_isMax (h₁ : a < b) (h₂ : ¬IsMax b) :
    Ioo a (succ b) = insert b (Ioo a b) := by
  simp_rw [← Iio_inter_Ioi, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ioi.2 h₁)]

Open Interval Characterization for Successor of Non-Maximal Element: $(a, \text{succ}(b)) = \{b\} \cup (a, b)$

Informal description

Let $\alpha$ be a preorder equipped with a successor function, and let $a, b \in \alpha$ such that $a < b$ and $b$ is not a maximal element. Then the open interval $(a, \text{succ}(b))$ is equal to the union of $\{b\}$ and the open interval $(a, b)$. In symbols: $$ (a, \text{succ}(b)) = \{b\} \cup (a, b) $$

Order.lt_succ_iff theorem

: a < succ b ↔ a ≤ b

Full source

@[simp]
theorem lt_succ_iff : a < succ b ↔ a ≤ b :=
  lt_succ_iff_of_not_isMax <| not_isMax b

Characterization of Strictly Below Successor: $a < \text{succ}(b) \leftrightarrow a \leq b$

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, $a$ is strictly less than the successor of $b$ if and only if $a$ is less than or equal to $b$. In symbols: $$ a < \text{succ}(b) \leftrightarrow a \leq b $$

Order.succ_le_succ_iff theorem

: succ a ≤ succ b ↔ a ≤ b

Full source

theorem succ_le_succ_iff : succsucc a ≤ succ b ↔ a ≤ b := by simp

Inequality Preservation under Successor Function: $\text{succ}(a) \leq \text{succ}(b) \leftrightarrow a \leq b$

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, the successor of $a$ is less than or equal to the successor of $b$ if and only if $a$ is less than or equal to $b$. That is, $\text{succ}(a) \leq \text{succ}(b) \leftrightarrow a \leq b$.

Order.succ_lt_succ_iff theorem

: succ a < succ b ↔ a < b

Full source

theorem succ_lt_succ_iff : succsucc a < succ b ↔ a < b := by simp

Strict Inequality Preservation under Successor Function

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, the successor of $a$ is strictly less than the successor of $b$ if and only if $a$ is strictly less than $b$. That is, $\text{succ}(a) < \text{succ}(b) \leftrightarrow a < b$.

Order.Iio_succ theorem

(a : α) : Iio (succ a) = Iic a

Full source

@[simp]
theorem Iio_succ (a : α) : Iio (succ a) = Iic a :=
  Iio_succ_of_not_isMax <| not_isMax _

Equality of Intervals for Successor: $(-\infty, \text{succ}(a)) = (-\infty, a]$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a successor function, the left-infinite right-open interval $(-\infty, \text{succ}(a))$ is equal to the left-infinite right-closed interval $(-\infty, a]$. In symbols: $$ (-\infty, \text{succ}(a)) = (-\infty, a] $$

Order.Ico_succ_right theorem

(a b : α) : Ico a (succ b) = Icc a b

Full source

@[simp]
theorem Ico_succ_right (a b : α) : Ico a (succ b) = Icc a b :=
  Ico_succ_right_of_not_isMax <| not_isMax _

Interval Equality for Successor: $[a, \text{succ}(b)) = [a, b]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, the left-closed right-open interval $[a, \text{succ}(b))$ is equal to the closed interval $[a, b]$. In symbols: $$ [a, \text{succ}(b)) = [a, b] $$

Order.Ioo_succ_right theorem

(a b : α) : Ioo a (succ b) = Ioc a b

Full source

@[simp]
theorem Ioo_succ_right (a b : α) : Ioo a (succ b) = Ioc a b :=
  Ioo_succ_right_of_not_isMax <| not_isMax _

Open Interval Equals Left-Open Right-Closed Interval under Successor

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, the open interval $(a, \text{succ}(b))$ is equal to the left-open right-closed interval $(a, b]$. In symbols: $$ (a, \text{succ}(b)) = (a, b] $$

Order.succ_eq_succ_iff theorem

: succ a = succ b ↔ a = b

Full source

@[simp]
theorem succ_eq_succ_iff : succsucc a = succ b ↔ a = b :=
  succ_eq_succ_iff_of_not_isMax (not_isMax a) (not_isMax b)

Injectivity of Successor Function in Ordered Types

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, the successor of $a$ equals the successor of $b$ if and only if $a$ equals $b$. In symbols: $$\text{succ}(a) = \text{succ}(b) \leftrightarrow a = b$$

Order.succ_injective theorem

: Injective (succ : α → α)

Full source

theorem succ_injective : Injective (succ : α → α) := fun _ _ => succ_eq_succ_iff.1

Injectivity of the Successor Function in Ordered Types

Informal description

The successor function $\text{succ} : \alpha \to \alpha$ in an ordered type $\alpha$ is injective, meaning that for any elements $a, b \in \alpha$, if $\text{succ}(a) = \text{succ}(b)$, then $a = b$.

Order.succ_ne_succ_iff theorem

: succ a ≠ succ b ↔ a ≠ b

Full source

theorem succ_ne_succ_iff : succsucc a ≠ succ bsucc a ≠ succ b ↔ a ≠ b :=
  succ_injective.ne_iff

Inequality Preservation by Successor Function: $\text{succ}(a) \neq \text{succ}(b) \leftrightarrow a \neq b$

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, the successor of $a$ is not equal to the successor of $b$ if and only if $a$ is not equal to $b$. In symbols: $$\text{succ}(a) \neq \text{succ}(b) \leftrightarrow a \neq b$$

Order.lt_succ_iff_eq_or_lt theorem

: a < succ b ↔ a = b ∨ a < b

Full source

theorem lt_succ_iff_eq_or_lt : a < succ b ↔ a = b ∨ a < b :=
  lt_succ_iff.trans le_iff_eq_or_lt

Characterization of Strictly Below Successor: $a < \text{succ}(b) \leftrightarrow a = b \lor a < b$

Informal description

For any elements $a$ and $b$ in an ordered type $\alpha$ equipped with a successor function, $a$ is strictly less than the successor of $b$ if and only if $a$ is equal to $b$ or $a$ is strictly less than $b$. In symbols: $$ a < \text{succ}(b) \leftrightarrow a = b \lor a < b $$

Order.Iio_succ_eq_insert theorem

(a : α) : Iio (succ a) = insert a (Iio a)

Full source

theorem Iio_succ_eq_insert (a : α) : Iio (succ a) = insert a (Iio a) :=
  Iio_succ_eq_insert_of_not_isMax <| not_isMax a

Interval Characterization: $(-\infty, \text{succ}(a)) = \{a\} \cup (-\infty, a)$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a successor function, the left-infinite right-open interval $(-\infty, \text{succ}(a))$ is equal to the union of $\{a\}$ and the interval $(-\infty, a)$. In symbols: $$ (-\infty, \text{succ}(a)) = \{a\} \cup (-\infty, a) $$

Order.Ico_succ_right_eq_insert theorem

(h : a ≤ b) : Ico a (succ b) = insert b (Ico a b)

Full source

theorem Ico_succ_right_eq_insert (h : a ≤ b) : Ico a (succ b) = insert b (Ico a b) :=
  Ico_succ_right_eq_insert_of_not_isMax h <| not_isMax b

Interval Decomposition for Successor: $[a, \text{succ}(b)) = \{b\} \cup [a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if $a \leq b$, then the left-closed right-open interval $[a, \text{succ}(b))$ is equal to the union of $\{b\}$ and the interval $[a, b)$. In symbols: $$ [a, \text{succ}(b)) = \{b\} \cup [a, b) $$

Order.Ioo_succ_right_eq_insert theorem

(h : a < b) : Ioo a (succ b) = insert b (Ioo a b)

Full source

theorem Ioo_succ_right_eq_insert (h : a < b) : Ioo a (succ b) = insert b (Ioo a b) :=
  Ioo_succ_right_eq_insert_of_not_isMax h <| not_isMax b

Open Interval Characterization for Successor: $(a, \text{succ}(b)) = \{b\} \cup (a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, if $a < b$, then the open interval $(a, \text{succ}(b))$ is equal to the union of $\{b\}$ and the open interval $(a, b)$. In symbols: $$ (a, \text{succ}(b)) = \{b\} \cup (a, b) $$

Order.Ioo_eq_empty_iff_le_succ theorem

: Ioo a b = ∅ ↔ b ≤ succ a

Full source

@[simp]
theorem Ioo_eq_empty_iff_le_succ : IooIoo a b = ∅ ↔ b ≤ succ a := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · contrapose! h
    exact ⟨succ a, lt_succ_iff_not_isMax.mpr (not_isMax a), h⟩
  · ext x
    suffices a < x → b ≤ x by simpa
    exact fun hx ↦ le_of_lt_succ <| lt_of_le_of_lt h <| succ_strictMono hx

Empty Open Interval Characterization via Successor: $(a, b) = \emptyset \leftrightarrow b \leq \text{succ}(a)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function, the open interval $(a, b)$ is empty if and only if $b$ is less than or equal to the successor of $a$, i.e., $(a, b) = \emptyset \leftrightarrow b \leq \text{succ}(a)$.

Order.lt_succ_bot_iff theorem

[NoMaxOrder α] : a < succ ⊥ ↔ a = ⊥

Full source

theorem lt_succ_bot_iff [NoMaxOrder α] : a < succ ⊥ ↔ a = ⊥ := by rw [lt_succ_iff, le_bot_iff]

Characterization of Elements Below Successor of Bottom: $a < \text{succ}(\bot) \leftrightarrow a = \bot$

Informal description

In an order $\alpha$ with no maximal elements, an element $a$ is strictly less than the successor of the bottom element $\bot$ if and only if $a$ is equal to $\bot$. That is, $a < \text{succ}(\bot) \leftrightarrow a = \bot$.

Order.le_succ_bot_iff theorem

: a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥

Full source

theorem le_succ_bot_iff : a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥ := by
  rw [le_succ_iff_eq_or_le, le_bot_iff, or_comm]

Characterization of Elements Below Successor of Bottom: $a \leq \text{succ}(\bot) \leftrightarrow a = \bot \lor a = \text{succ}(\bot)$

Informal description

For any element $a$ in an order with a bottom element $\bot$ and a successor function, $a$ is less than or equal to the successor of $\bot$ if and only if $a$ equals $\bot$ or $a$ equals the successor of $\bot$. In symbols: $$ a \leq \text{succ}(\bot) \leftrightarrow a = \bot \lor a = \text{succ}(\bot) $$

Order.instSubsingletonSuccOrder instance

[PartialOrder α] : Subsingleton (SuccOrder α)

Full source

/-- There is at most one way to define the successors in a `PartialOrder`. -/
instance [PartialOrder α] : Subsingleton (SuccOrder α) :=
  ⟨by
    intro h₀ h₁
    ext a
    by_cases ha : IsMax a
    · exact (@IsMax.succ_eq _ _ h₀ _ ha).trans ha.succ_eq.symm
    · exact @CovBy.succ_eq _ _ h₀ _ _ (covBy_succ_of_not_isMax ha)⟩

Uniqueness of Successor Order Structure on Partial Orders

Informal description

For any partially ordered set $\alpha$, there is at most one way to define a successor order structure on $\alpha$.

Order.succ_eq_sInf theorem

[CompleteLattice α] [SuccOrder α] (a : α) : succ a = sInf (Set.Ioi a)

Full source

theorem succ_eq_sInf [CompleteLattice α] [SuccOrder α] (a : α) :
    succ a = sInf (Set.Ioi a) := by
  apply (le_sInf fun b => succ_le_of_lt).antisymm
  obtain rfl | ha := eq_or_ne a ⊤
  · rw [succ_top]
    exact le_top
  · exact sInf_le (lt_succ_iff_ne_top.2 ha)

Successor as Infimum of Strictly Greater Elements in Complete Lattice

Informal description

Let $\alpha$ be a complete lattice equipped with a successor order structure. For any element $a \in \alpha$, the successor of $a$ equals the infimum of the set of all elements strictly greater than $a$, i.e., \[ \text{succ}(a) = \inf \{b \in \alpha \mid a < b\}. \]

Order.succ_eq_iInf theorem

[CompleteLattice α] [SuccOrder α] (a : α) : succ a = ⨅ b > a, b

Full source

theorem succ_eq_iInf [CompleteLattice α] [SuccOrder α] (a : α) : succ a = ⨅ b > a, b := by
  rw [succ_eq_sInf, iInf_subtype', iInf, Subtype.range_coe_subtype, Ioi]

Successor as Infimum of Strictly Greater Elements in Complete Lattice

Informal description

Let $\alpha$ be a complete lattice equipped with a successor order structure. For any element $a \in \alpha$, the successor of $a$ is equal to the infimum of all elements $b \in \alpha$ such that $b > a$, i.e., \[ \text{succ}(a) = \inf_{b > a} b. \]

Order.succ_eq_csInf theorem

[ConditionallyCompleteLattice α] [SuccOrder α] [NoMaxOrder α] (a : α) : succ a = sInf (Set.Ioi a)

Full source

theorem succ_eq_csInf [ConditionallyCompleteLattice α] [SuccOrder α] [NoMaxOrder α] (a : α) :
    succ a = sInf (Set.Ioi a) := by
  apply (le_csInf nonempty_Ioi fun b => succ_le_of_lt).antisymm
  exact csInf_le ⟨a, fun b => le_of_lt⟩ <| lt_succ a

Successor as Infimum of Strictly Greater Elements in Conditionally Complete Lattice

Informal description

Let $\alpha$ be a conditionally complete lattice equipped with a successor order structure and no maximal element. For any element $a \in \alpha$, the successor of $a$ equals the infimum of the set of all elements strictly greater than $a$, i.e., \[ \text{succ}(a) = \inf \{b \in \alpha \mid a < b\}. \]

Order.pred definition

: α → α

Full source

/-- 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`. -/
def pred : α → α :=
  PredOrder.pred

Predecessor function

Informal description

The predecessor function on a preorder $\alpha$ equipped with a `PredOrder` structure. For any element $a \in \alpha$, if $a$ is not minimal, then $\mathrm{pred}(a)$ is the greatest element less than $a$. If $a$ is minimal, then $\mathrm{pred}(a) = a$.

Order.pred_le theorem

: ∀ a : α, pred a ≤ a

Full source

theorem pred_le : ∀ a : α, pred a ≤ a :=
  PredOrder.pred_le

Predecessor is Less Than or Equal to Element

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessor of $a$ is less than or equal to $a$, i.e., $\mathrm{pred}(a) \leq a$.

Order.min_of_le_pred theorem

{a : α} : a ≤ pred a → IsMin a

Full source

theorem min_of_le_pred {a : α} : a ≤ pred a → IsMin a :=
  PredOrder.min_of_le_pred

Minimality Criterion via Predecessor

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a \leq \mathrm{pred}(a)$, then $a$ is a minimal element in $\alpha$.

Order.le_pred_of_lt theorem

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

Full source

theorem le_pred_of_lt {a b : α} : a < b → a ≤ pred b :=
  PredOrder.le_pred_of_lt

Predecessor Bound for Strictly Lesser Elements

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a < b$, then $a$ is less than or equal to the predecessor of $b$, i.e., $a \leq \mathrm{pred}(b)$.

Order.le_pred_iff_isMin theorem

: a ≤ pred a ↔ IsMin a

Full source

@[simp]
theorem le_pred_iff_isMin : a ≤ pred a ↔ IsMin a :=
  ⟨min_of_le_pred, fun h => h <| pred_le _⟩

Minimality Criterion via Predecessor Inequality: $a \leq \mathrm{pred}(a) \leftrightarrow \text{IsMin}(a)$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the inequality $a \leq \mathrm{pred}(a)$ holds if and only if $a$ is a minimal element in $\alpha$.

Order.pred_lt_iff_not_isMin theorem

: pred a < a ↔ ¬IsMin a

Full source

@[simp]
theorem pred_lt_iff_not_isMin : predpred a < a ↔ ¬IsMin a :=
  ⟨not_isMin_of_lt, fun ha => (pred_le a).lt_of_not_le fun h => ha <| min_of_le_pred h⟩

Predecessor Strictly Less Than Element if and only if Not Minimal

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessor of $a$ is strictly less than $a$ if and only if $a$ is not a minimal element in $\alpha$, i.e., $\mathrm{pred}(a) < a \leftrightarrow \neg \text{IsMin}(a)$.

Order.pred_wcovBy theorem

(a : α) : pred a ⩿ a

Full source

theorem pred_wcovBy (a : α) : predpred a ⩿ a :=
  ⟨pred_le a, fun _ hb nh => (le_pred_of_lt nh).not_lt hb⟩

Predecessor Weakly Covers Element

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessor of $a$ is weakly covered by $a$, denoted as $\mathrm{pred}(a) ⩿ a$. This means that there is no element strictly between $\mathrm{pred}(a)$ and $a$ in the order.

Order.pred_covBy_of_not_isMin theorem

(h : ¬IsMin a) : pred a ⋖ a

Full source

theorem pred_covBy_of_not_isMin (h : ¬IsMin a) : predpred a ⋖ a :=
  (pred_wcovBy a).covBy_of_lt <| pred_lt_of_not_isMin h

Predecessor Covers Non-Minimal Element

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a$ is not minimal, then its predecessor $\mathrm{pred}(a)$ is covered by $a$, denoted as $\mathrm{pred}(a) \lessdot a$. This means there is no element strictly between $\mathrm{pred}(a)$ and $a$ in the order.

Order.pred_lt_of_not_isMin_of_le theorem

(ha : ¬IsMin a) : a ≤ b → pred a < b

Full source

theorem pred_lt_of_not_isMin_of_le (ha : ¬IsMin a) : a ≤ b → pred a < b :=
  (pred_lt_of_not_isMin ha).trans_le

Predecessor Strictly Less Than Greater Element for Non-Minimal Elements

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a$ is not minimal and $a \leq b$, then $\mathrm{pred}(a) < b$.

Order.le_pred_iff_of_not_isMin theorem

(ha : ¬IsMin a) : b ≤ pred a ↔ b < a

Full source

theorem le_pred_iff_of_not_isMin (ha : ¬IsMin a) : b ≤ pred a ↔ b < a :=
  ⟨fun h => h.trans_lt <| pred_lt_of_not_isMin ha, le_pred_of_lt⟩

Predecessor Characterization for Non-Minimal Elements

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a$ is not minimal, then an element $b$ satisfies $b \leq \mathrm{pred}(a)$ if and only if $b < a$.

Order.pred_lt_pred_of_not_isMin theorem

(h : a < b) (ha : ¬IsMin a) : pred a < pred b

Full source

lemma pred_lt_pred_of_not_isMin (h : a < b) (ha : ¬ IsMin a) : pred a < pred b :=
  pred_lt_of_not_isMin_of_le ha <| le_pred_of_lt h

Predecessor Function Preserves Strict Order for Non-Minimal Elements

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a$ is not minimal and $a < b$, then $\mathrm{pred}(a) < \mathrm{pred}(b)$.

Order.pred_le_pred_of_not_isMin_of_le theorem

(ha : ¬IsMin a) (hb : ¬IsMin b) : a ≤ b → pred a ≤ pred b

Full source

theorem pred_le_pred_of_not_isMin_of_le (ha : ¬IsMin a) (hb : ¬IsMin b) :
    a ≤ b → pred a ≤ pred b := by
  rw [le_pred_iff_of_not_isMin hb]
  apply pred_lt_of_not_isMin_of_le ha

Monotonicity of Predecessor for Non-Minimal Elements

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if neither $a$ nor $b$ is minimal, then $a \leq b$ implies $\mathrm{pred}(a) \leq \mathrm{pred}(b)$.

Order.pred_le_pred theorem

{a b : α} (h : a ≤ b) : pred a ≤ pred b

Full source

@[simp, mono, gcongr]
theorem pred_le_pred {a b : α} (h : a ≤ b) : pred a ≤ pred b :=
  succ_le_succ h.dual

Monotonicity of the Predecessor Function

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a \leq b$, then $\mathrm{pred}(a) \leq \mathrm{pred}(b)$.

Order.pred_mono theorem

: Monotone (pred : α → α)

Full source

theorem pred_mono : Monotone (pred : α → α) := fun _ _ => pred_le_pred

Monotonicity of the Predecessor Function

Informal description

The predecessor function $\mathrm{pred} : \alpha \to \alpha$ on a preorder $\alpha$ equipped with a `PredOrder` structure is monotone. That is, for any elements $a, b \in \alpha$, if $a \leq b$, then $\mathrm{pred}(a) \leq \mathrm{pred}(b)$.

Order.pred_le_of_wcovBy theorem

(h : a ⩿ b) : pred b ≤ a

Full source

/-- See also `Order.pred_eq_of_covBy`. -/
lemma pred_le_of_wcovBy (h : a ⩿ b) : pred b ≤ a := by
  obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le
  · by_contra hba
    exact h.2 (hab.lt.le_pred.lt_of_not_le hba) (pred_lt_of_not_isMin hab.lt.not_isMin)
  · exact (pred_le _).trans hba

Predecessor Inequality under Weak Covering Relation

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function, if $a$ is weakly covered by $b$ (denoted $a \ ⩿ \ b$), then the predecessor of $b$ is less than or equal to $a$, i.e., $\mathrm{pred}(b) \leq a$.

Order.pred_iterate_le theorem

(k : ℕ) (x : α) : pred^[k] x ≤ x

Full source

theorem pred_iterate_le (k : ℕ) (x : α) : predpred^[k] x ≤ x := by
  conv_rhs => rw [(by simp only [Function.iterate_id, id] : x = id^[k] x)]
  exact Monotone.iterate_le_of_le pred_mono pred_le k x

Iterated Predecessor is Less Than or Equal to Original Element

Informal description

For any natural number $k$ and any element $x$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the $k$-th iterate of $\mathrm{pred}$ applied to $x$ is less than or equal to $x$, i.e., $\mathrm{pred}^k(x) \leq x$.

Order.isMin_iterate_pred_of_eq_of_lt theorem

{n m : ℕ} (h_eq : pred^[n] a = pred^[m] a) (h_lt : n < m) : IsMin (pred^[n] a)

Full source

theorem isMin_iterate_pred_of_eq_of_lt {n m : ℕ} (h_eq : predpred^[n] a = predpred^[m] a)
    (h_lt : n < m) : IsMin (predpred^[n] a) :=
  @isMax_iterate_succ_of_eq_of_lt αᵒᵈ _ _ _ _ _ h_eq h_lt

Minimality of Iterated Predecessor at Equal Points with $n < m$

Informal description

For any natural numbers $n$ and $m$ and any element $a$ in a preorder $\alpha$ with a predecessor function, if the $n$-th iterate of the predecessor function applied to $a$ equals the $m$-th iterate (i.e., $\mathrm{pred}^n(a) = \mathrm{pred}^m(a)$) and $n < m$, then the element $\mathrm{pred}^n(a)$ is minimal in $\alpha$.

Order.isMin_iterate_pred_of_eq_of_ne theorem

{n m : ℕ} (h_eq : pred^[n] a = pred^[m] a) (h_ne : n ≠ m) : IsMin (pred^[n] a)

Full source

theorem isMin_iterate_pred_of_eq_of_ne {n m : ℕ} (h_eq : predpred^[n] a = predpred^[m] a)
    (h_ne : n ≠ m) : IsMin (predpred^[n] a) :=
  @isMax_iterate_succ_of_eq_of_ne αᵒᵈ _ _ _ _ _ h_eq h_ne

Minimality of Iterated Predecessor at Equal Points with Distinct Iteration Counts

Informal description

For any natural numbers $n$ and $m$ and any element $a$ in a preorder $\alpha$ with a predecessor function, if the $n$-th iterate of the predecessor function applied to $a$ equals the $m$-th iterate (i.e., $\mathrm{pred}^n(a) = \mathrm{pred}^m(a)$) and $n \neq m$, then the element $\mathrm{pred}^n(a)$ is minimal in $\alpha$.

Order.Ici_subset_Ioi_pred_of_not_isMin theorem

(ha : ¬IsMin a) : Ici a ⊆ Ioi (pred a)

Full source

theorem Ici_subset_Ioi_pred_of_not_isMin (ha : ¬IsMin a) : IciIci a ⊆ Ioi (pred a) :=
  fun _ ↦ pred_lt_of_not_isMin_of_le ha

Inclusion of Closed Interval in Open Predcessor Interval for Non-Minimal Elements

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a$ is not minimal, then the left-closed right-infinite interval $[a, \infty)$ is contained in the left-open right-infinite interval $(\mathrm{pred}(a), \infty)$.

Order.Iic_pred_of_not_isMin theorem

(ha : ¬IsMin a) : Iic (pred a) = Iio a

Full source

theorem Iic_pred_of_not_isMin (ha : ¬IsMin a) : Iic (pred a) = Iio a :=
  Set.ext fun _ => le_pred_iff_of_not_isMin ha

Characterization of Predecessor Interval for Non-Minimal Elements

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a$ is not minimal, then the left-infinite right-closed interval $(-\infty, \mathrm{pred}(a)]$ is equal to the left-infinite right-open interval $(-\infty, a)$. In other words, $\{x \mid x \leq \mathrm{pred}(a)\} = \{x \mid x < a\}$.

Order.Icc_subset_Ioc_pred_left_of_not_isMin theorem

(ha : ¬IsMin a) : Icc a b ⊆ Ioc (pred a) b

Full source

theorem Icc_subset_Ioc_pred_left_of_not_isMin (ha : ¬IsMin a) : IccIcc a b ⊆ Ioc (pred a) b := by
 rw [← Ioi_inter_Iic, ← Ici_inter_Iic]
 gcongr
 apply Ici_subset_Ioi_pred_of_not_isMin ha

Inclusion of $[a, b]$ in $(\mathrm{pred}(a), b]$ for non-minimal $a$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a$ is not minimal, then the closed interval $[a, b]$ is contained in the left-open right-closed interval $(\mathrm{pred}(a), b]$.

Order.Ico_subset_Ioo_pred_left_of_not_isMin theorem

(ha : ¬IsMin a) : Ico a b ⊆ Ioo (pred a) b

Full source

theorem Ico_subset_Ioo_pred_left_of_not_isMin (ha : ¬IsMin a) : IcoIco a b ⊆ Ioo (pred a) b  := by
  rw [← Ioi_inter_Iio, ← Ici_inter_Iio]
  gcongr
  apply Ici_subset_Ioi_pred_of_not_isMin ha

Inclusion of $[a, b)$ in $(\mathrm{pred}(a), b)$ for non-minimal $a$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a$ is not minimal, then the left-closed right-open interval $[a, b)$ is contained in the left-open right-open interval $(\mathrm{pred}(a), b)$.

Order.Icc_pred_right_of_not_isMin theorem

(ha : ¬IsMin b) : Icc a (pred b) = Ico a b

Full source

theorem Icc_pred_right_of_not_isMin (ha : ¬IsMin b) : Icc a (pred b) = Ico a b := by
  rw [← Ici_inter_Iic, Iic_pred_of_not_isMin ha, Ici_inter_Iio]

Closed Interval Equals Half-Open Interval via Predecessor for Non-Minimal Elements

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $b$ is not minimal, then the closed interval $[a, \mathrm{pred}(b)]$ is equal to the left-closed right-open interval $[a, b)$. In other words: $$ [a, \mathrm{pred}(b)] = [a, b) $$

Order.Ioc_pred_right_of_not_isMin theorem

(ha : ¬IsMin b) : Ioc a (pred b) = Ioo a b

Full source

theorem Ioc_pred_right_of_not_isMin (ha : ¬IsMin b) : Ioc a (pred b) = Ioo a b := by
  rw [← Ioi_inter_Iic, Iic_pred_of_not_isMin ha, Ioi_inter_Iio]

Equality of Intervals: $(a, \mathrm{pred}(b)] = (a, b)$ for Non-Minimal $b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $b$ is not minimal, then the left-open right-closed interval $(a, \mathrm{pred}(b)]$ is equal to the open interval $(a, b)$. In symbols: $$ (a, \mathrm{pred}(b)] = (a, b) $$

Order.pred_lt theorem

(a : α) : pred a < a

Full source

theorem pred_lt (a : α) : pred a < a :=
  pred_lt_of_not_isMin <| not_isMin a

Predecessor is Strictly Less Than Element in Non-Minimal Case

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a$ is not minimal, then $\mathrm{pred}(a) < a$.

Order.pred_lt_of_le theorem

: a ≤ b → pred a < b

Full source

@[simp]
theorem pred_lt_of_le : a ≤ b → pred a < b :=
  pred_lt_of_not_isMin_of_le <| not_isMin a

Predecessor Strictly Less Than Greater Element

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a \leq b$, then $\mathrm{pred}(a) < b$.

Order.le_pred_iff theorem

: a ≤ pred b ↔ a < b

Full source

@[simp]
theorem le_pred_iff : a ≤ pred b ↔ a < b :=
  le_pred_iff_of_not_isMin <| not_isMin b

Predecessor Characterization: $a \leq \mathrm{pred}(b) \leftrightarrow a < b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the inequality $a \leq \mathrm{pred}(b)$ holds if and only if $a < b$.

Order.pred_le_pred_of_le theorem

: a ≤ b → pred a ≤ pred b

Full source

theorem pred_le_pred_of_le : a ≤ b → pred a ≤ pred b := by intro; simp_all

Monotonicity of Predecessor Function

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a \leq b$, then $\mathrm{pred}(a) \leq \mathrm{pred}(b)$.

Order.pred_lt_pred theorem

: a < b → pred a < pred b

Full source

theorem pred_lt_pred : a < b → pred a < pred b := by intro; simp_all

Strict Monotonicity of the Predecessor Function

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a < b$, then $\mathrm{pred}(a) < \mathrm{pred}(b)$.

Order.pred_strictMono theorem

: StrictMono (pred : α → α)

Full source

theorem pred_strictMono : StrictMono (pred : α → α) := fun _ _ => pred_lt_pred

Strict Monotonicity of the Predecessor Function

Informal description

The predecessor function $\mathrm{pred} : \alpha \to \alpha$ on a preorder $\alpha$ equipped with a `PredOrder` structure is strictly monotone. That is, for any elements $a, b \in \alpha$, if $a < b$, then $\mathrm{pred}(a) < \mathrm{pred}(b)$.

Order.pred_covBy theorem

(a : α) : pred a ⋖ a

Full source

theorem pred_covBy (a : α) : predpred a ⋖ a :=
  pred_covBy_of_not_isMin <| not_isMin a

Predecessor Covers Element in Preorder

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessor $\mathrm{pred}(a)$ is covered by $a$, denoted as $\mathrm{pred}(a) \lessdot a$. This means there is no element strictly between $\mathrm{pred}(a)$ and $a$ in the order.

Order.Ici_subset_Ioi_pred theorem

(a : α) : Ici a ⊆ Ioi (pred a)

Full source

theorem Ici_subset_Ioi_pred (a : α) : IciIci a ⊆ Ioi (pred a) := by simp

Inclusion of Intervals: $[a, \infty) \subseteq (\mathrm{pred}(a), \infty)$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the left-closed right-infinite interval $[a, \infty)$ is contained in the left-open right-infinite interval $(\mathrm{pred}(a), \infty)$. In other words, for any $x \in \alpha$, if $a \leq x$, then $\mathrm{pred}(a) < x$.

Order.Iic_pred theorem

(a : α) : Iic (pred a) = Iio a

Full source

@[simp]
theorem Iic_pred (a : α) : Iic (pred a) = Iio a :=
  Iic_pred_of_not_isMin <| not_isMin a

Characterization of Predecessor Interval: $(-\infty, \mathrm{pred}(a)] = (-\infty, a)$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the left-infinite right-closed interval $(-\infty, \mathrm{pred}(a)]$ is equal to the left-infinite right-open interval $(-\infty, a)$. In other words, $\{x \mid x \leq \mathrm{pred}(a)\} = \{x \mid x < a\}$.

Order.Icc_subset_Ioc_pred_left theorem

(a b : α) : Icc a b ⊆ Ioc (pred a) b

Full source

@[simp]
theorem Icc_subset_Ioc_pred_left (a b : α) : IccIcc a b ⊆ Ioc (pred a) b :=
  Icc_subset_Ioc_pred_left_of_not_isMin <| not_isMin _

Inclusion of $[a, b]$ in $(\mathrm{pred}(a), b]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the closed interval $[a, b]$ is contained in the left-open right-closed interval $(\mathrm{pred}(a), b]$. In other words, for any $x \in \alpha$, if $a \leq x \leq b$, then $\mathrm{pred}(a) < x \leq b$.

Order.Ico_subset_Ioo_pred_left theorem

(a b : α) : Ico a b ⊆ Ioo (pred a) b

Full source

@[simp]
theorem Ico_subset_Ioo_pred_left (a b : α) : IcoIco a b ⊆ Ioo (pred a) b :=
  Ico_subset_Ioo_pred_left_of_not_isMin <| not_isMin _

Inclusion of $[a, b)$ in $(\mathrm{pred}(a), b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the left-closed right-open interval $[a, b)$ is contained in the left-open right-open interval $(\mathrm{pred}(a), b)$.

Order.Icc_pred_right theorem

(a b : α) : Icc a (pred b) = Ico a b

Full source

@[simp]
theorem Icc_pred_right (a b : α) : Icc a (pred b) = Ico a b :=
  Icc_pred_right_of_not_isMin <| not_isMin _

Closed Interval Equals Half-Open Interval via Predecessor

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the closed interval $[a, \mathrm{pred}(b)]$ is equal to the left-closed right-open interval $[a, b)$. That is, $$ [a, \mathrm{pred}(b)] = [a, b). $$

Order.Ioc_pred_right theorem

(a b : α) : Ioc a (pred b) = Ioo a b

Full source

@[simp]
theorem Ioc_pred_right (a b : α) : Ioc a (pred b) = Ioo a b :=
  Ioc_pred_right_of_not_isMin <| not_isMin _

Equality of Intervals: $(a, \mathrm{pred}(b)] = (a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the left-open right-closed interval $(a, \mathrm{pred}(b)]$ is equal to the open interval $(a, b)$. In symbols: $$ (a, \mathrm{pred}(b)] = (a, b) $$

Order.pred_eq_iff_isMin theorem

: pred a = a ↔ IsMin a

Full source

@[simp]
theorem pred_eq_iff_isMin : predpred a = a ↔ IsMin a :=
  ⟨fun h => min_of_le_pred h.ge, fun h => h.eq_of_le <| pred_le _⟩

Predecessor Equals Element if and only if Minimal

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessor of $a$ equals $a$ if and only if $a$ is a minimal element in $\alpha$. In other words, $\mathrm{pred}(a) = a \leftrightarrow \text{IsMin}(a)$.

Order.le_iff_eq_or_le_pred theorem

: a ≤ b ↔ a = b ∨ a ≤ pred b

Full source

lemma le_iff_eq_or_le_pred : a ≤ b ↔ a = b ∨ a ≤ pred b := by
  by_cases hb : IsMin b
  · simpa [hb.pred_eq] using le_of_eq
  · rw [le_pred_iff_of_not_isMin hb, le_iff_eq_or_lt]

Characterization of Order Relation via Predecessor: $a \leq b \leftrightarrow (a = b \lor a \leq \mathrm{pred}(b))$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the inequality $a \leq b$ holds if and only if either $a = b$ or $a \leq \mathrm{pred}(b)$.

Order.pred_le_le_iff theorem

{a b : α} : pred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = pred a

Full source

theorem pred_le_le_iff {a b : α} : predpred a ≤ b ∧ b ≤ apred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = pred a := by
  refine
    ⟨fun h =>
      or_iff_not_imp_left.2 fun hba : b ≠ a => (le_pred_of_lt <| h.2.lt_of_ne hba).antisymm h.1, ?_⟩
  rintro (rfl | rfl)
  · exact ⟨pred_le b, le_rfl⟩
  · exact ⟨le_rfl, pred_le a⟩

Characterization of Elements Between Predecessor and Original Element

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the inequalities $\mathrm{pred}(a) \leq b$ and $b \leq a$ hold if and only if $b$ is equal to $a$ or $b$ is equal to $\mathrm{pred}(a)$.

Order.pred_eq_of_covBy theorem

(h : a ⋖ b) : pred b = a

Full source

/-- See also `Order.pred_le_of_wcovBy`. -/
lemma pred_eq_of_covBy (h : a ⋖ b) : pred b = a := h.wcovBy.pred_le.antisymm (le_pred_of_lt h.lt)

Predecessor of Covered Element Equals Covering Element

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a$ is covered by $b$ (denoted $a \lessdot b$), then the predecessor of $b$ equals $a$, i.e., $\mathrm{pred}(b) = a$.

OrderIso.map_pred theorem

{β : Type*} [PartialOrder β] [PredOrder β] (f : α ≃o β) (a : α) : f (pred a) = pred (f a)

Full source

theorem _root_.OrderIso.map_pred {β : Type*} [PartialOrder β] [PredOrder β] (f : α ≃o β) (a : α) :
    f (pred a) = pred (f a) :=
  f.dual.map_succ a

Order Isomorphism Preserves Predecessor: $f(\mathrm{pred}(a)) = \mathrm{pred}(f(a))$

Informal description

Let $\alpha$ and $\beta$ be partially ordered sets, where $\beta$ is equipped with a predecessor order structure. For any order isomorphism $f : \alpha \simeq \beta$ and any element $a \in \alpha$, the image of the predecessor of $a$ under $f$ equals the predecessor of the image of $a$ under $f$, i.e., $f(\mathrm{pred}(a)) = \mathrm{pred}(f(a))$.

Order.pred_eq_iff_covBy theorem

: pred b = a ↔ a ⋖ b

Full source

theorem pred_eq_iff_covBy : predpred b = a ↔ a ⋖ b :=
  ⟨by
    rintro rfl
    exact pred_covBy _, CovBy.pred_eq⟩

Predecessor-Covering Equivalence: $\mathrm{pred}(b) = a \leftrightarrow a \lessdot b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessor of $b$ equals $a$ if and only if $a$ is covered by $b$ (i.e., $a \lessdot b$). In other words, $\mathrm{pred}(b) = a \leftrightarrow a \lessdot b$.

Order.pred_bot theorem

: pred (⊥ : α) = ⊥

Full source

@[simp]
theorem pred_bot : pred (⊥ : α) = ⊥ :=
  isMin_bot.pred_eq

Predecessor of Bottom Element is Bottom

Informal description

In an ordered type $\alpha$ with a bottom element $\bot$ and a predecessor function $\mathrm{pred}$, the predecessor of the bottom element is itself, i.e., $\mathrm{pred}(\bot) = \bot$.

Order.le_pred_iff_eq_bot theorem

: a ≤ pred a ↔ a = ⊥

Full source

theorem le_pred_iff_eq_bot : a ≤ pred a ↔ a = ⊥ :=
  @succ_le_iff_eq_top αᵒᵈ _ _ _ _

Minimality Criterion via Predecessor: $a \leq \mathrm{pred}(a) \leftrightarrow a = \bot$

Informal description

For any element $a$ in an ordered type $\alpha$ with a bottom element $\bot$ and a predecessor function $\mathrm{pred}$, the inequality $a \leq \mathrm{pred}(a)$ holds if and only if $a$ is equal to the bottom element $\bot$.

Order.pred_lt_iff_ne_bot theorem

: pred a < a ↔ a ≠ ⊥

Full source

theorem pred_lt_iff_ne_bot : predpred a < a ↔ a ≠ ⊥ :=
  @lt_succ_iff_ne_top αᵒᵈ _ _ _ _

Predecessor Strictly Less Than Element if and only if Not Bottom

Informal description

For any element $a$ in an ordered type $\alpha$ with a bottom element $\bot$ and a predecessor function $\mathrm{pred}$, the predecessor of $a$ is strictly less than $a$ if and only if $a$ is not equal to $\bot$, i.e., $\mathrm{pred}(a) < a \leftrightarrow a \neq \bot$.

Order.pred_lt_top theorem

(a : α) : pred a < ⊤

Full source

theorem pred_lt_top (a : α) : pred a < ⊤ :=
  (pred_mono le_top).trans_lt <| pred_lt_of_not_isMin not_isMin_top

Predecessor is Strictly Below Top Element

Informal description

For any element $a$ in an ordered type $\alpha$ with a top element $\top$ and a predecessor function $\mathrm{pred}$, the predecessor of $a$ is strictly less than $\top$, i.e., $\mathrm{pred}(a) < \top$.

Order.pred_ne_top theorem

(a : α) : pred a ≠ ⊤

Full source

theorem pred_ne_top (a : α) : predpred a ≠ ⊤ :=
  (pred_lt_top a).ne

Predecessor is Not Top Element

Informal description

For any element $a$ in an ordered type $\alpha$ with a top element $\top$ and a predecessor function $\mathrm{pred}$, the predecessor of $a$ is not equal to $\top$, i.e., $\mathrm{pred}(a) \neq \top$.

Order.le_of_pred_lt theorem

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

Full source

theorem le_of_pred_lt {a b : α} : pred a < b → a ≤ b := fun h ↦ by
  by_contra! nh
  exact le_pred_of_lt nh |>.trans_lt h |>.false

Implication from Predecessor Strict Inequality to Non-strict Inequality

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if the predecessor of $a$ is strictly less than $b$, then $a$ is less than or equal to $b$, i.e., $\mathrm{pred}(a) < b \implies a \leq b$.

Order.pred_lt_iff_of_not_isMin theorem

(ha : ¬IsMin a) : pred a < b ↔ a ≤ b

Full source

theorem pred_lt_iff_of_not_isMin (ha : ¬IsMin a) : predpred a < b ↔ a ≤ b :=
  ⟨le_of_pred_lt, (pred_lt_of_not_isMin ha).trans_le⟩

Predecessor Strict Inequality Equivalence for Non-Minimal Elements

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a$ is not minimal (i.e., $\neg \mathrm{IsMin}(a)$), then the predecessor of $a$ is strictly less than $b$ if and only if $a$ is less than or equal to $b$. In other words: \[ \mathrm{pred}(a) < b \leftrightarrow a \leq b. \]

Order.pred_lt_pred_iff_of_not_isMin theorem

(ha : ¬IsMin a) (hb : ¬IsMin b) : pred a < pred b ↔ a < b

Full source

theorem pred_lt_pred_iff_of_not_isMin (ha : ¬IsMin a) (hb : ¬IsMin b) :
    predpred a < pred b ↔ a < b := by
  rw [pred_lt_iff_of_not_isMin ha, le_pred_iff_of_not_isMin hb]

Predecessor Strict Inequality Preserves Order for Non-Minimal Elements

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if neither $a$ nor $b$ is minimal, then the predecessor of $a$ is strictly less than the predecessor of $b$ if and only if $a$ is strictly less than $b$. In other words: \[ \mathrm{pred}(a) < \mathrm{pred}(b) \leftrightarrow a < b. \]

Order.pred_le_pred_iff_of_not_isMin theorem

(ha : ¬IsMin a) (hb : ¬IsMin b) : pred a ≤ pred b ↔ a ≤ b

Full source

theorem pred_le_pred_iff_of_not_isMin (ha : ¬IsMin a) (hb : ¬IsMin b) :
    predpred a ≤ pred b ↔ a ≤ b := by
  rw [le_pred_iff_of_not_isMin hb, pred_lt_iff_of_not_isMin ha]

Predecessor Order-Preserving Property for Non-Minimal Elements

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if neither $a$ nor $b$ is minimal, then the predecessor of $a$ is less than or equal to the predecessor of $b$ if and only if $a \leq b$. In other words: \[ \mathrm{pred}(a) \leq \mathrm{pred}(b) \leftrightarrow a \leq b. \]

Order.Ioi_pred_of_not_isMin theorem

(ha : ¬IsMin a) : Ioi (pred a) = Ici a

Full source

theorem Ioi_pred_of_not_isMin (ha : ¬IsMin a) : Ioi (pred a) = Ici a :=
  Set.ext fun _ => pred_lt_iff_of_not_isMin ha

Equality of Intervals for Non-Minimal Elements: $(\mathrm{pred}(a), \infty) = [a, \infty)$

Informal description

For any non-minimal element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the left-open right-infinite interval $(\mathrm{pred}(a), \infty)$ is equal to the left-closed right-infinite interval $[a, \infty)$. In other words: \[ \{x \in \alpha \mid \mathrm{pred}(a) < x\} = \{x \in \alpha \mid a \leq x\}. \]

Order.Ioc_pred_left_of_not_isMin theorem

(ha : ¬IsMin a) : Ioc (pred a) b = Icc a b

Full source

theorem Ioc_pred_left_of_not_isMin (ha : ¬IsMin a) : Ioc (pred a) b = Icc a b := by
  rw [← Ioi_inter_Iic, Ioi_pred_of_not_isMin ha, Ici_inter_Iic]

Equality of Intervals: $(\mathrm{pred}(a), b] = [a, b]$ for Non-Minimal $a$

Informal description

For any non-minimal element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, and for any element $b \in \alpha$, the left-open right-closed interval $(\mathrm{pred}(a), b]$ is equal to the closed interval $[a, b]$. In other words: \[ \{x \in \alpha \mid \mathrm{pred}(a) < x \leq b\} = \{x \in \alpha \mid a \leq x \leq b\}. \]

Order.Ioo_pred_left_of_not_isMin theorem

(ha : ¬IsMin a) : Ioo (pred a) b = Ico a b

Full source

theorem Ioo_pred_left_of_not_isMin (ha : ¬IsMin a) : Ioo (pred a) b = Ico a b := by
  rw [← Ioi_inter_Iio, Ioi_pred_of_not_isMin ha, Ici_inter_Iio]

Open Interval Equals Half-Open Interval via Predecessor: $(\mathrm{pred}(a), b) = [a, b)$ for Non-Minimal $a$

Informal description

For any non-minimal element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the open interval $(\mathrm{pred}(a), b)$ is equal to the left-closed right-open interval $[a, b)$. In other words: \[ \{x \in \alpha \mid \mathrm{pred}(a) < x < b\} = \{x \in \alpha \mid a \leq x < b\}. \]

Order.pred_eq_pred_iff_of_not_isMin theorem

(ha : ¬IsMin a) (hb : ¬IsMin b) : pred a = pred b ↔ a = b

Full source

theorem pred_eq_pred_iff_of_not_isMin (ha : ¬IsMin a) (hb : ¬IsMin b) :
    predpred a = pred b ↔ a = b := by
  rw [eq_iff_le_not_lt, eq_iff_le_not_lt, pred_le_pred_iff_of_not_isMin ha hb,
    pred_lt_pred_iff_of_not_isMin ha hb]

Predecessor Equality Characterization for Non-Minimal Elements

Informal description

For any non-minimal elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessors of $a$ and $b$ are equal if and only if $a$ and $b$ are equal. In other words: \[ \mathrm{pred}(a) = \mathrm{pred}(b) \leftrightarrow a = b. \]

Order.pred_le_iff_eq_or_le theorem

: pred a ≤ b ↔ b = pred a ∨ a ≤ b

Full source

theorem pred_le_iff_eq_or_le : predpred a ≤ b ↔ b = pred a ∨ a ≤ b := by
  by_cases ha : IsMin a
  · rw [ha.pred_eq, or_iff_right_of_imp ge_of_eq]
  · rw [← pred_lt_iff_of_not_isMin ha, le_iff_eq_or_lt, eq_comm]

Predecessor Inequality Characterization: $\mathrm{pred}(a) \leq b \leftrightarrow (b = \mathrm{pred}(a) \lor a \leq b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessor of $a$ is less than or equal to $b$ if and only if either $b$ equals the predecessor of $a$ or $a$ is less than or equal to $b$. In other words: \[ \mathrm{pred}(a) \leq b \leftrightarrow (b = \mathrm{pred}(a) \lor a \leq b). \]

Order.pred_lt_iff_eq_or_lt_of_not_isMin theorem

(ha : ¬IsMin a) : pred a < b ↔ a = b ∨ a < b

Full source

theorem pred_lt_iff_eq_or_lt_of_not_isMin (ha : ¬IsMin a) : predpred a < b ↔ a = b ∨ a < b :=
  (pred_lt_iff_of_not_isMin ha).trans le_iff_eq_or_lt

Predecessor Strict Inequality Characterization for Non-Minimal Elements

Informal description

For any non-minimal element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessor of $a$ is strictly less than $b$ if and only if either $a = b$ or $a < b$. In other words: \[ \mathrm{pred}(a) < b \leftrightarrow (a = b \lor a < b). \]

Order.not_isMax_pred theorem

[Nontrivial α] (a : α) : ¬IsMax (pred a)

Full source

theorem not_isMax_pred [Nontrivial α] (a : α) : ¬ IsMax (pred a) :=
  not_isMin_succ (α := αᵒᵈ) a

Predecessor is Not Maximal in Nontrivial Order

Informal description

In a nontrivial preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessor of any element $a \in \alpha$ is not a maximal element. That is, $\neg \text{IsMax}(\mathrm{pred}(a))$ for all $a \in \alpha$.

Order.Ici_pred theorem

(a : α) : Ici (pred a) = insert (pred a) (Ici a)

Full source

theorem Ici_pred (a : α) : Ici (pred a) = insert (pred a) (Ici a) :=
  ext fun _ => pred_le_iff_eq_or_le

Decomposition of Interval Above Predecessor: $[\mathrm{pred}(a), \infty) = \{\mathrm{pred}(a)\} \cup [a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the left-closed right-infinite interval $[\mathrm{pred}(a), \infty)$ is equal to the union of the singleton set $\{\mathrm{pred}(a)\}$ and the interval $[a, \infty)$. In other words: \[ [\mathrm{pred}(a), \infty) = \{\mathrm{pred}(a)\} \cup [a, \infty). \]

Order.Ioi_pred_eq_insert_of_not_isMin theorem

(ha : ¬IsMin a) : Ioi (pred a) = insert a (Ioi a)

Full source

theorem Ioi_pred_eq_insert_of_not_isMin (ha : ¬IsMin a) : Ioi (pred a) = insert a (Ioi a) := by
  ext x; simp only [insert, mem_setOf, @eq_comm _ x a, mem_Ioi, Set.insert]
  exact pred_lt_iff_eq_or_lt_of_not_isMin ha

Decomposition of Interval Above Predecessor for Non-Minimal Elements

Informal description

For any non-minimal element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the left-open right-infinite interval $(\mathrm{pred}(a), \infty)$ is equal to the union of $\{a\}$ and the interval $(a, \infty)$. In other words: \[ (\mathrm{pred}(a), \infty) = \{a\} \cup (a, \infty). \]

Order.Icc_pred_left theorem

(h : pred a ≤ b) : Icc (pred a) b = insert (pred a) (Icc a b)

Full source

theorem Icc_pred_left (h : pred a ≤ b) : Icc (pred a) b = insert (pred a) (Icc a b) := by
  simp_rw [← Ici_inter_Iic, Ici_pred, insert_inter_of_mem (mem_Iic.2 h)]

Decomposition of Closed Interval via Predecessor: $[\mathrm{pred}(a), b] = \{\mathrm{pred}(a)\} \cup [a, b]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $\mathrm{pred}(a) \leq b$, then the closed interval $[\mathrm{pred}(a), b]$ is equal to the union of the singleton set $\{\mathrm{pred}(a)\}$ and the interval $[a, b]$. In other words: \[ [\mathrm{pred}(a), b] = \{\mathrm{pred}(a)\} \cup [a, b]. \]

Order.Ico_pred_left theorem

(h : pred a < b) : Ico (pred a) b = insert (pred a) (Ico a b)

Full source

theorem Ico_pred_left (h : pred a < b) : Ico (pred a) b = insert (pred a) (Ico a b) := by
  simp_rw [← Ici_inter_Iio, Ici_pred, insert_inter_of_mem (mem_Iio.2 h)]

Decomposition of Left-Closed Right-Open Interval via Predecessor

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $\mathrm{pred}(a) < b$, then the left-closed right-open interval $[\mathrm{pred}(a), b)$ is equal to the union of $\{\mathrm{pred}(a)\}$ and the interval $[a, b)$. In other words: \[ [\mathrm{pred}(a), b) = \{\mathrm{pred}(a)\} \cup [a, b). \]

Order.pred_lt_iff theorem

: pred a < b ↔ a ≤ b

Full source

@[simp]
theorem pred_lt_iff : predpred a < b ↔ a ≤ b :=
  pred_lt_iff_of_not_isMin <| not_isMin a

Predecessor Strict Inequality Equivalence

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessor of $a$ is strictly less than $b$ if and only if $a$ is less than or equal to $b$. In other words: \[ \mathrm{pred}(a) < b \leftrightarrow a \leq b. \]

Order.pred_le_pred_iff theorem

: pred a ≤ pred b ↔ a ≤ b

Full source

theorem pred_le_pred_iff : predpred a ≤ pred b ↔ a ≤ b := by simp

Predecessor Function Preserves Order

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the inequality $\mathrm{pred}(a) \leq \mathrm{pred}(b)$ holds if and only if $a \leq b$.

Order.pred_lt_pred_iff theorem

: pred a < pred b ↔ a < b

Full source

theorem pred_lt_pred_iff : predpred a < pred b ↔ a < b := by simp

Predecessor Function Preserves Strict Order

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the inequality $\mathrm{pred}(a) < \mathrm{pred}(b)$ holds if and only if $a < b$.

Order.Ioi_pred theorem

(a : α) : Ioi (pred a) = Ici a

Full source

@[simp]
theorem Ioi_pred (a : α) : Ioi (pred a) = Ici a :=
  Ioi_pred_of_not_isMin <| not_isMin a

Equality of Intervals for Predecessor Function: $(\mathrm{pred}(a), \infty) = [a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the left-open right-infinite interval $(\mathrm{pred}(a), \infty)$ is equal to the left-closed right-infinite interval $[a, \infty)$. In other words: \[ \{x \in \alpha \mid \mathrm{pred}(a) < x\} = \{x \in \alpha \mid a \leq x\}. \]

Order.Ioc_pred_left theorem

(a b : α) : Ioc (pred a) b = Icc a b

Full source

@[simp]
theorem Ioc_pred_left (a b : α) : Ioc (pred a) b = Icc a b :=
  Ioc_pred_left_of_not_isMin <| not_isMin _

Equality of Intervals: $(\mathrm{pred}(a), b] = [a, b]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the left-open right-closed interval $(\mathrm{pred}(a), b]$ is equal to the closed interval $[a, b]$. That is: \[ \{x \in \alpha \mid \mathrm{pred}(a) < x \leq b\} = \{x \in \alpha \mid a \leq x \leq b\}. \]

Order.Ioo_pred_left theorem

(a b : α) : Ioo (pred a) b = Ico a b

Full source

@[simp]
theorem Ioo_pred_left (a b : α) : Ioo (pred a) b = Ico a b :=
  Ioo_pred_left_of_not_isMin <| not_isMin _

Open Interval Equals Half-Open Interval via Predecessor: $(\mathrm{pred}(a), b) = [a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the open interval $(\mathrm{pred}(a), b)$ is equal to the left-closed right-open interval $[a, b)$. In other words: \[ \{x \in \alpha \mid \mathrm{pred}(a) < x < b\} = \{x \in \alpha \mid a \leq x < b\}. \]

Order.pred_eq_pred_iff theorem

: pred a = pred b ↔ a = b

Full source

@[simp]
theorem pred_eq_pred_iff : predpred a = pred b ↔ a = b := by
  simp_rw [eq_iff_le_not_lt, pred_le_pred_iff, pred_lt_pred_iff]

Predecessor Function is Injective

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the equality $\mathrm{pred}(a) = \mathrm{pred}(b)$ holds if and only if $a = b$.

Order.pred_injective theorem

: Injective (pred : α → α)

Full source

theorem pred_injective : Injective (pred : α → α) := fun _ _ => pred_eq_pred_iff.1

Injectivity of the Predecessor Function

Informal description

The predecessor function $\mathrm{pred} : \alpha \to \alpha$ on a preorder $\alpha$ equipped with a `PredOrder` structure is injective, meaning that for any elements $a, b \in \alpha$, if $\mathrm{pred}(a) = \mathrm{pred}(b)$, then $a = b$.

Order.pred_ne_pred_iff theorem

: pred a ≠ pred b ↔ a ≠ b

Full source

theorem pred_ne_pred_iff : predpred a ≠ pred bpred a ≠ pred b ↔ a ≠ b :=
  pred_injective.ne_iff

Inequality Preservation by Predecessor Function

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the inequality $\mathrm{pred}(a) \neq \mathrm{pred}(b)$ holds if and only if $a \neq b$.

Order.pred_lt_iff_eq_or_lt theorem

: pred a < b ↔ a = b ∨ a < b

Full source

theorem pred_lt_iff_eq_or_lt : predpred a < b ↔ a = b ∨ a < b :=
  pred_lt_iff.trans le_iff_eq_or_lt

Predecessor Strict Inequality Characterization: $\mathrm{pred}(a) < b \leftrightarrow a = b \lor a < b$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the strict inequality $\mathrm{pred}(a) < b$ holds if and only if either $a = b$ or $a < b$.

Order.Ioi_pred_eq_insert theorem

(a : α) : Ioi (pred a) = insert a (Ioi a)

Full source

theorem Ioi_pred_eq_insert (a : α) : Ioi (pred a) = insert a (Ioi a) :=
  ext fun _ => pred_lt_iff_eq_or_lt.trans <| or_congr_left eq_comm

Characterization of Interval Above Predecessor: $(\mathrm{pred}(a), \infty) = \{a\} \cup (a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the left-open right-infinite interval $(\mathrm{pred}(a), \infty)$ is equal to the union of $\{a\}$ and the interval $(a, \infty)$. In other words: $$ \{x \in \alpha \mid \mathrm{pred}(a) < x\} = \{a\} \cup \{x \in \alpha \mid a < x\}. $$

Order.Ico_pred_right_eq_insert theorem

(h : a ≤ b) : Ioc (pred a) b = insert a (Ioc a b)

Full source

theorem Ico_pred_right_eq_insert (h : a ≤ b) : Ioc (pred a) b = insert a (Ioc a b) := by
  simp_rw [← Ioi_inter_Iic, Ioi_pred_eq_insert, insert_inter_of_mem (mem_Iic.2 h)]

Characterization of Interval Above Predecessor: $(\mathrm{pred}(a), b] = \{a\} \cup (a, b]$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a \leq b$, then the left-open right-closed interval $(\mathrm{pred}(a), b]$ is equal to the union of $\{a\}$ and the interval $(a, b]$. In other words: $$ \{x \in \alpha \mid \mathrm{pred}(a) < x \leq b\} = \{a\} \cup \{x \in \alpha \mid a < x \leq b\}. $$

Order.Ioo_pred_right_eq_insert theorem

(h : a < b) : Ioo (pred a) b = insert a (Ioo a b)

Full source

theorem Ioo_pred_right_eq_insert (h : a < b) : Ioo (pred a) b = insert a (Ioo a b) := by
  simp_rw [← Ioi_inter_Iio, Ioi_pred_eq_insert, insert_inter_of_mem (mem_Iio.2 h)]

Open Interval Above Predecessor Equals Insertion of Element: $(\mathrm{pred}(a), b) = \{a\} \cup (a, b)$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $a < b$, then the open interval $(\mathrm{pred}(a), b)$ is equal to the union of $\{a\}$ and the interval $(a, b)$. In other words: $$ \{x \in \alpha \mid \mathrm{pred}(a) < x < b\} = \{a\} \cup \{x \in \alpha \mid a < x < b\}. $$

Order.Ioo_eq_empty_iff_pred_le theorem

: Ioo a b = ∅ ↔ pred b ≤ a

Full source

@[simp]
theorem Ioo_eq_empty_iff_pred_le : IooIoo a b = ∅ ↔ pred b ≤ a := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · contrapose! h
    exact ⟨pred b, h, pred_lt_iff_not_isMin.mpr (not_isMin b)⟩
  · ext x
    suffices a < x → b ≤ x by simpa
    exact fun hx ↦ le_of_pred_lt <| lt_of_le_of_lt h hx

Empty Open Interval Criterion: $(a, b) = \emptyset \leftrightarrow \mathrm{pred}(b) \leq a$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the open interval $(a, b)$ is empty if and only if the predecessor of $b$ is less than or equal to $a$, i.e., $(a, b) = \emptyset \leftrightarrow \mathrm{pred}(b) \leq a$.

Order.pred_top_lt_iff theorem

[NoMinOrder α] : pred ⊤ < a ↔ a = ⊤

Full source

theorem pred_top_lt_iff [NoMinOrder α] : predpred ⊤ < a ↔ a = ⊤ :=
  @lt_succ_bot_iff αᵒᵈ _ _ _ _ _

Predecessor of Top Element is Strictly Below Only Top Element in NoMinOrder

Informal description

In a preorder $\alpha$ with no minimal elements, the predecessor of the top element $\top$ is strictly less than an element $a$ if and only if $a$ is equal to $\top$, i.e., $\mathrm{pred}(\top) < a \leftrightarrow a = \top$.

Order.pred_top_le_iff theorem

: pred ⊤ ≤ a ↔ a = ⊤ ∨ a = pred ⊤

Full source

theorem pred_top_le_iff : predpred ⊤ ≤ a ↔ a = ⊤ ∨ a = pred ⊤ :=
  @le_succ_bot_iff αᵒᵈ _ _ _ _

Characterization of Elements Above Predecessor of Top: $\mathrm{pred}(\top) \leq a \leftrightarrow a = \top \lor a = \mathrm{pred}(\top)$

Informal description

For any element $a$ in an order with a top element $\top$ and a predecessor function, the predecessor of $\top$ is less than or equal to $a$ if and only if $a$ equals $\top$ or $a$ equals the predecessor of $\top$. In symbols: $$ \mathrm{pred}(\top) \leq a \leftrightarrow a = \top \lor a = \mathrm{pred}(\top) $$

Order.instSubsingletonPredOrder instance

[PartialOrder α] : Subsingleton (PredOrder α)

Full source

/-- There is at most one way to define the predecessors in a `PartialOrder`. -/
instance [PartialOrder α] : Subsingleton (PredOrder α) :=
  ⟨by
    intro h₀ h₁
    ext a
    by_cases ha : IsMin a
    · exact (@IsMin.pred_eq _ _ h₀ _ ha).trans ha.pred_eq.symm
    · exact @CovBy.pred_eq _ _ h₀ _ _ (pred_covBy_of_not_isMin ha)⟩

Uniqueness of Predecessor Order in Partial Orders

Informal description

For any partially ordered set $\alpha$, there is at most one way to define a predecessor order structure on $\alpha$.

Order.pred_eq_sSup theorem

[CompleteLattice α] [PredOrder α] : ∀ a : α, pred a = sSup (Set.Iio a)

Full source

theorem pred_eq_sSup [CompleteLattice α] [PredOrder α] :
    ∀ a : α, pred a = sSup (Set.Iio a) :=
  succ_eq_sInf (α := αᵒᵈ)

Predecessor as Supremum of Strictly Lesser Elements in Complete Lattice

Informal description

Let $\alpha$ be a complete lattice equipped with a predecessor order structure. For any element $a \in \alpha$, the predecessor of $a$ equals the supremum of the set of all elements strictly less than $a$, i.e., \[ \mathrm{pred}(a) = \sup \{b \in \alpha \mid b < a\}. \]

Order.pred_eq_iSup theorem

[CompleteLattice α] [PredOrder α] (a : α) : pred a = ⨆ b < a, b

Full source

theorem pred_eq_iSup [CompleteLattice α] [PredOrder α] (a : α) : pred a = ⨆ b < a, b :=
  succ_eq_iInf (α := αᵒᵈ) a

Predecessor as Supremum of Strictly Lesser Elements in Complete Lattice

Informal description

Let $\alpha$ be a complete lattice equipped with a predecessor order structure. For any element $a \in \alpha$, the predecessor of $a$ is equal to the supremum of all elements $b \in \alpha$ such that $b < a$, i.e., \[ \mathrm{pred}(a) = \sup_{b < a} b. \]

Order.pred_eq_csSup theorem

[ConditionallyCompleteLattice α] [PredOrder α] [NoMinOrder α] (a : α) : pred a = sSup (Set.Iio a)

Full source

theorem pred_eq_csSup [ConditionallyCompleteLattice α] [PredOrder α] [NoMinOrder α] (a : α) :
    pred a = sSup (Set.Iio a) :=
  succ_eq_csInf (α := αᵒᵈ) a

Predecessor as Supremum of Strictly Lesser Elements in Conditionally Complete Lattice

Informal description

Let $\alpha$ be a conditionally complete lattice equipped with a predecessor order structure and no minimal element. For any element $a \in \alpha$, the predecessor of $a$ equals the supremum of the set of all elements strictly less than $a$, i.e., \[ \mathrm{pred}(a) = \sup \{b \in \alpha \mid b < a\}. \]

Order.le_succ_pred theorem

(a : α) : a ≤ succ (pred a)

Full source

lemma le_succ_pred (a : α) : a ≤ succ (pred a) := (pred_wcovBy _).le_succ

Element is Bounded Above by Successor of Predecessor

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a successor function $\mathrm{succ}$ and a predecessor function $\mathrm{pred}$, the element $a$ is less than or equal to the successor of its predecessor, i.e., $a \leq \mathrm{succ}(\mathrm{pred}(a))$.

Order.pred_succ_le theorem

(a : α) : pred (succ a) ≤ a

Full source

lemma pred_succ_le (a : α) : pred (succ a) ≤ a := (wcovBy_succ _).pred_le

Predecessor of Successor is Below Original Element

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a successor function $\mathrm{succ}$ and a predecessor function $\mathrm{pred}$, the predecessor of the successor of $a$ is less than or equal to $a$, i.e., $\mathrm{pred}(\mathrm{succ}(a)) \leq a$.

Order.pred_le_iff_le_succ theorem

: pred a ≤ b ↔ a ≤ succ b

Full source

lemma pred_le_iff_le_succ : predpred a ≤ b ↔ a ≤ succ b where
  mp hab := (le_succ_pred _).trans (succ_mono hab)
  mpr hab := (pred_mono hab).trans (pred_succ_le _)

Galois Connection Between Predecessor and Successor Functions

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$ equipped with a successor function $\mathrm{succ}$ and a predecessor function $\mathrm{pred}$, the predecessor of $a$ is less than or equal to $b$ if and only if $a$ is less than or equal to the successor of $b$, i.e., $\mathrm{pred}(a) \leq b \leftrightarrow a \leq \mathrm{succ}(b)$.

Order.gc_pred_succ theorem

: GaloisConnection (pred : α → α) succ

Full source

lemma gc_pred_succ : GaloisConnection (pred : α → α) succ := fun _ _ ↦ pred_le_iff_le_succ

Galois Connection Between Predecessor and Successor Functions

Informal description

For a preorder $\alpha$ equipped with successor and predecessor functions $\mathrm{succ}$ and $\mathrm{pred}$, the pair $(\mathrm{pred}, \mathrm{succ})$ forms a Galois connection. That is, for any elements $a, b \in \alpha$, we have $\mathrm{pred}(a) \leq b$ if and only if $a \leq \mathrm{succ}(b)$.

Order.succ_pred_of_not_isMin theorem

(h : ¬IsMin a) : succ (pred a) = a

Full source

@[simp]
theorem succ_pred_of_not_isMin (h : ¬IsMin a) : succ (pred a) = a :=
  CovBy.succ_eq (pred_covBy_of_not_isMin h)

Successor of Predecessor Equals Original Element for Non-Minimal Elements

Informal description

For any element $a$ in a preorder $\alpha$ equipped with successor and predecessor functions, if $a$ is not minimal, then the successor of its predecessor equals $a$, i.e., $\mathrm{succ}(\mathrm{pred}(a)) = a$.

Order.pred_succ_of_not_isMax theorem

(h : ¬IsMax a) : pred (succ a) = a

Full source

@[simp]
theorem pred_succ_of_not_isMax (h : ¬IsMax a) : pred (succ a) = a :=
  CovBy.pred_eq (covBy_succ_of_not_isMax h)

Predecessor of Successor for Non-Maximal Elements: $\mathrm{pred}(\mathrm{succ}(a)) = a$

Informal description

For any element $a$ in an ordered type $\alpha$ equipped with a successor function, if $a$ is not a maximal element, then the predecessor of its successor equals $a$, i.e., $\mathrm{pred}(\mathrm{succ}(a)) = a$.

Order.succ_pred theorem

[NoMinOrder α] (a : α) : succ (pred a) = a

Full source

theorem succ_pred [NoMinOrder α] (a : α) : succ (pred a) = a :=
  CovBy.succ_eq (pred_covBy _)

Successor of Predecessor Equals Original Element in NoMinOrder

Informal description

For any element $a$ in a preorder $\alpha$ with no minimal elements, the successor of the predecessor of $a$ equals $a$, i.e., $\mathrm{succ}(\mathrm{pred}(a)) = a$.

Order.pred_succ theorem

[NoMaxOrder α] (a : α) : pred (succ a) = a

Full source

theorem pred_succ [NoMaxOrder α] (a : α) : pred (succ a) = a :=
  CovBy.pred_eq (covBy_succ _)

Predecessor-Successor Identity in NoMaxOrder: $\mathrm{pred}(\mathrm{succ}(a)) = a$

Informal description

For any element $a$ in a preorder $\alpha$ with no maximal elements, the predecessor of the successor of $a$ is equal to $a$, i.e., $\mathrm{pred}(\mathrm{succ}(a)) = a$.

Order.pred_succ_iterate_of_not_isMax theorem

(i : α) (n : ℕ) (hin : ¬IsMax (succ^[n - 1] i)) : pred^[n] (succ^[n] i) = i

Full source

theorem pred_succ_iterate_of_not_isMax (i : α) (n : ℕ) (hin : ¬IsMax (succ^[n - 1] i)) :
    predpred^[n] (succsucc^[n] i) = i := by
  induction' n with n hn
  · simp only [Nat.zero_eq, Function.iterate_zero, id]
  rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hin
  have h_not_max : ¬IsMax (succ^[n - 1] i) := by
    rcases n with - | n
    · simpa using hin
    rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hn ⊢
    have h_sub_le : succsucc^[n] i ≤ succsucc^[n.succ] i := by
      rw [Function.iterate_succ']
      exact le_succ _
    refine fun h_max => hin fun j hj => ?_
    have hj_le : j ≤ succsucc^[n] i := h_max (h_sub_le.trans hj)
    exact hj_le.trans h_sub_le
  rw [Function.iterate_succ, Function.iterate_succ']
  simp only [Function.comp_apply]
  rw [pred_succ_of_not_isMax hin]
  exact hn h_not_max

Iterated Predecessor-Successor Identity for Non-Maximal Elements: $\mathrm{pred}^n(\mathrm{succ}^n(i)) = i$

Informal description

For any element $i$ in a preorder $\alpha$ equipped with successor and predecessor functions, and for any natural number $n$, if the $(n-1)$-th iterate of the successor function applied to $i$ is not maximal, then the $n$-th iterate of the predecessor function applied to the $n$-th iterate of the successor function applied to $i$ equals $i$, i.e., $\mathrm{pred}^n(\mathrm{succ}^n(i)) = i$.

Order.succ_pred_iterate_of_not_isMin theorem

(i : α) (n : ℕ) (hin : ¬IsMin (pred^[n - 1] i)) : succ^[n] (pred^[n] i) = i

Full source

theorem succ_pred_iterate_of_not_isMin (i : α) (n : ℕ) (hin : ¬IsMin (pred^[n - 1] i)) :
    succsucc^[n] (predpred^[n] i) = i :=
  @pred_succ_iterate_of_not_isMax αᵒᵈ _ _ _ i n hin

Iterated Successor-Predecessor Identity for Non-Minimal Elements: $\mathrm{succ}^n(\mathrm{pred}^n(i)) = i$

Informal description

For any element $i$ in a preorder $\alpha$ equipped with successor and predecessor functions, and for any natural number $n$, if the $(n-1)$-th iterate of the predecessor function applied to $i$ is not minimal, then the $n$-th iterate of the successor function applied to the $n$-th iterate of the predecessor function applied to $i$ equals $i$, i.e., $\mathrm{succ}^n(\mathrm{pred}^n(i)) = i$.

WithTop.instSuccOrder instance

: SuccOrder (WithTop α)

Full source

instance : SuccOrder (WithTop α) where
  succ a :=
    match a with
    | ⊤ => ⊤
    | Option.some a => ite (succ a = a) ⊤ (some (succ a))
  le_succ a := by
    obtain - | a := a
    · exact le_top
    change _ ≤ ite _ _ _
    split_ifs
    · exact le_top
    · exact coe_le_coe.2 (le_succ a)
  max_of_succ_le {a} ha := by
    cases a
    · exact isMax_top
    dsimp only at ha
    split_ifs at ha with ha'
    · exact (not_top_le_coe _ ha).elim
    · rw [coe_le_coe, succ_le_iff_isMax, ← succ_eq_iff_isMax] at ha
      exact (ha' ha).elim
  succ_le_of_lt {a b} h := by
    cases b
    · exact le_top
    cases a
    · exact (not_top_lt h).elim
    rw [coe_lt_coe] at h
    change ite _ _ _ ≤ _
    split_ifs with ha
    · rw [succ_eq_iff_isMax] at ha
      exact (ha.not_lt h).elim
    · exact coe_le_coe.2 (succ_le_of_lt h)

Successor Order on `WithTop` of a Successor Order

Informal description

For any preorder $\alpha$ equipped with a successor function (i.e., a `SuccOrder`), the type `WithTop α` (obtained by adding a top element to $\alpha$) inherits a natural successor order structure. The successor function on `WithTop α` is defined such that: - For a non-maximal element $a \in \alpha$, the successor of $a$ in `WithTop α` is the successor of $a$ in $\alpha$. - For a maximal element $a \in \alpha$, the successor of $a$ in `WithTop α` is the top element $\top$. - The top element $\top$ is its own successor. This construction preserves the properties of the successor function from $\alpha$ while correctly handling the new maximal element $\top$.

WithTop.succ_coe_of_isMax theorem

{a : α} (h : IsMax a) : succ ↑a = (⊤ : WithTop α)

Full source

@[simp]
theorem succ_coe_of_isMax {a : α} (h : IsMax a) : succ ↑a = (⊤ : WithTop α) :=
  dif_pos (succ_eq_iff_isMax.2 h)

Successor of Maximal Element in `WithTop` is Top

Informal description

For any element $a$ in a preorder $\alpha$ that is maximal (i.e., $\text{IsMax}(a)$ holds), the successor of $a$ in the type `WithTop α` (obtained by adding a top element to $\alpha$) is the top element $\top$. In other words, $\text{succ}(a) = \top$.

WithTop.succ_coe_of_not_isMax theorem

{a : α} (h : ¬IsMax a) : succ (↑a : WithTop α) = ↑(succ a)

Full source

theorem succ_coe_of_not_isMax {a : α} (h : ¬ IsMax a) : succ (↑a : WithTop α) = ↑(succ a) :=
  dif_neg (succ_eq_iff_isMax.not.2 h)

Successor of Non-Maximal Element in $\mathrm{WithTop}\ \alpha$

Informal description

For any element $a$ of type $\alpha$ that is not maximal, the successor of the image of $a$ in $\mathrm{WithTop}\ \alpha$ is equal to the image of the successor of $a$ in $\alpha$. In other words, if $a$ is not maximal, then $\mathrm{succ}(a) = \mathrm{succ}(a)$ under the embedding into $\mathrm{WithTop}\ \alpha$.

WithTop.succ_coe theorem

[NoMaxOrder α] {a : α} : succ (↑a : WithTop α) = ↑(succ a)

Full source

@[simp]
theorem succ_coe [NoMaxOrder α] {a : α} : succ (↑a : WithTop α) = ↑(succ a) :=
  succ_coe_of_not_isMax <| not_isMax a

Successor Preservation in $\mathrm{WithTop}\ \alpha$ for NoMaxOrder $\alpha$

Informal description

For any element $a$ in a preorder $\alpha$ with no maximal elements (i.e., $\alpha$ is a `NoMaxOrder`), the successor of the image of $a$ in $\mathrm{WithTop}\ \alpha$ is equal to the image of the successor of $a$ in $\alpha$. In other words, $\mathrm{succ}(a) = \mathrm{succ}(a)$ under the embedding into $\mathrm{WithTop}\ \alpha$.

WithTop.instPredOrder instance

: PredOrder (WithTop α)

Full source

instance : PredOrder (WithTop α) where
  pred a :=
    match a with
    | ⊤ => some ⊤
    | Option.some a => some (pred a)
  pred_le a :=
    match a with
    | ⊤ => le_top
    | Option.some a => coe_le_coe.2 (pred_le a)
  min_of_le_pred {a} ha := by
    cases a
    · exact ((coe_lt_top (⊤ : α)).not_le ha).elim
    · exact (min_of_le_pred <| coe_le_coe.1 ha).withTop
  le_pred_of_lt {a b} h := by
    cases a
    · exact (le_top.not_lt h).elim
    cases b
    · exact coe_le_coe.2 le_top
    exact coe_le_coe.2 (le_pred_of_lt <| coe_lt_coe.1 h)

Predecessor Order Structure on $\mathrm{WithTop}\ \alpha$

Informal description

For any preorder $\alpha$ equipped with a predecessor order structure, the type $\mathrm{WithTop}\ \alpha$ (obtained by adding a top element to $\alpha$) inherits a predecessor order structure. The predecessor of the top element is itself, and for any element $a \in \alpha$, the predecessor of its image in $\mathrm{WithTop}\ \alpha$ is the image of its predecessor in $\alpha$.

WithTop.orderPred_top theorem

: pred (⊤ : WithTop α) = ↑(⊤ : α)

Full source

/-- Not to be confused with `WithTop.pred_bot`, which is about `WithTop.pred`. -/
@[simp] lemma orderPred_top : pred (⊤ : WithTop α) = ↑(⊤ : α) := rfl

Predecessor of Top Element in $\mathrm{WithTop}\ \alpha$

Informal description

For a type $\alpha$ with a top element $\top$ and a predecessor order structure, the predecessor of the top element in $\mathrm{WithTop}\ \alpha$ is equal to the image of the top element of $\alpha$ under the coercion map, i.e., $\mathrm{pred}(\top) = \uparrow \top$.

WithTop.orderPred_coe theorem

(a : α) : pred (↑a : WithTop α) = ↑(pred a)

Full source

/-- Not to be confused with `WithTop.pred_coe`, which is about `WithTop.pred`. -/
@[simp] lemma orderPred_coe (a : α) : pred (↑a : WithTop α) = ↑(pred a) := rfl

Predecessor Commutes with Coercion to $\mathrm{WithTop}$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a predecessor order structure, the predecessor of the image of $a$ in $\mathrm{WithTop}\ \alpha$ (obtained by the coercion $\uparrow$) is equal to the image of the predecessor of $a$ in $\alpha$. In other words, if $\mathrm{pred}$ denotes the predecessor function, then: $$\mathrm{pred}(\uparrow a) = \uparrow (\mathrm{pred}(a))$$

WithTop.pred_untop theorem

: ∀ (a : WithTop α) (ha : a ≠ ⊤), pred (a.untop ha) = (pred a).untop (by induction a <;> simp)

Full source

@[simp]
theorem pred_untop :
    ∀ (a : WithTop α) (ha : a ≠ ⊤),
      pred (a.untop ha) = (pred a).untop (by induction a <;> simp)
  | ⊤, ha => (ha rfl).elim
  | (a : α), _ => rfl

Predecessor Commutes with Untop Operation in WithTop

Informal description

For any element $a$ in $\mathrm{WithTop}\ \alpha$ that is not equal to the top element $\top$, the predecessor of the underlying element (obtained via `untop`) equals the underlying element of the predecessor of $a$. In other words, if $a \in \mathrm{WithTop}\ \alpha$ with $a \neq \top$, then: $$\mathrm{pred}(a.\mathrm{untop}) = (\mathrm{pred}(a)).\mathrm{untop}$$

WithTop.instIsEmptyPredOrderOfNonempty instance

[hα : Nonempty α] : IsEmpty (PredOrder (WithTop α))

Full source

instance [hα : Nonempty α] : IsEmpty (PredOrder (WithTop α)) :=
  ⟨by
    intro
    cases h : pred (⊤ : WithTop α) with
    | top => exact hα.elim fun a => (min_of_le_pred h.ge).not_lt <| coe_lt_top a
    | coe a =>
      obtain ⟨c, hc⟩ := exists_gt a
      rw [← coe_lt_coe, ← h] at hc
      exact (le_pred_of_lt (coe_lt_top c)).not_lt hc⟩

Nonexistence of Predecessor Order on WithTop for Nonempty Types

Informal description

For any nonempty type $\alpha$ with a preorder, there is no predecessor order structure on $\text{WithTop}\ \alpha$ (the type obtained by adding a top element to $\alpha$). In other words, the typeclass `PredOrder (WithTop α)` is empty.

WithBot.instSuccOrder instance

: SuccOrder (WithBot α)

Full source

instance : SuccOrder (WithBot α) where
  succ a :=
    match a with
    | ⊥ => some ⊥
    | Option.some a => some (succ a)
  le_succ a :=
    match a with
    | ⊥ => bot_le
    | Option.some a => coe_le_coe.2 (le_succ a)
  max_of_succ_le {a} ha := by
    cases a
    · exact ((bot_lt_coe (⊥ : α)).not_le ha).elim
    · exact (max_of_succ_le <| coe_le_coe.1 ha).withBot
  succ_le_of_lt {a b} h := by
    cases b
    · exact (not_lt_bot h).elim
    cases a
    · exact coe_le_coe.2 bot_le
    · exact coe_le_coe.2 (succ_le_of_lt <| coe_lt_coe.1 h)

Successor Order Structure on WithBot

Informal description

For any type $\alpha$ with a preorder and a successor order structure, the type `WithBot α` (obtained by adding a bottom element to $\alpha$) inherits a successor order structure where: - The successor of the bottom element $\bot$ is $\bot$ itself - The successor of an element $a$ (when lifted to `WithBot α`) is the successor of $a$ in $\alpha$ (also lifted) This preserves the successor structure from $\alpha$ when adding a bottom element.

WithBot.orderSucc_bot theorem

: succ (⊥ : WithBot α) = ↑(⊥ : α)

Full source

/-- Not to be confused with `WithBot.succ_bot`, which is about `WithBot.succ`. -/
@[simp] lemma orderSucc_bot : succ (⊥ : WithBot α) = ↑(⊥ : α) := rfl

Successor of Bottom Element in `WithBot` Structure

Informal description

In a successor order structure on `WithBot α`, the successor of the bottom element `⊥` is equal to the lift of the bottom element of `α`. That is, $\mathrm{succ}(\bot) = \bot$ when viewed in `WithBot α$.

WithBot.orderSucc_coe theorem

(a : α) : succ (↑a : WithBot α) = ↑(succ a)

Full source

/-- Not to be confused with `WithBot.succ_coe`, which is about `WithBot.succ`. -/
@[simp] lemma orderSucc_coe (a : α) : succ (↑a : WithBot α) = ↑(succ a) := rfl

Successor of Lifted Element in $\mathrm{WithBot}~\alpha$

Informal description

For any element $a$ of type $\alpha$, the successor of the lift of $a$ to $\mathrm{WithBot}~\alpha$ is equal to the lift of the successor of $a$ in $\alpha$. In other words, $\mathrm{succ}(a) = \mathrm{succ}(a)$ when viewed in $\mathrm{WithBot}~\alpha$.

WithBot.succ_unbot theorem

: ∀ (a : WithBot α) (ha : a ≠ ⊥), succ (a.unbot ha) = (succ a).unbot (by induction a <;> simp)

Full source

@[simp]
theorem succ_unbot :
    ∀ (a : WithBot α) (ha : a ≠ ⊥),
      succ (a.unbot ha) = (succ a).unbot (by induction a <;> simp)
  | ⊥, ha => (ha rfl).elim
  | (a : α), _ => rfl

Compatibility of Successor and `unbot` in $\mathrm{WithBot}~\alpha$

Informal description

For any element $a$ in $\mathrm{WithBot}~\alpha$ that is not the bottom element $\bot$, the successor of the underlying element (obtained via `unbot`) equals the underlying element of the successor of $a$. That is, $\mathrm{succ}(a.\mathrm{unbot}) = (\mathrm{succ}\,a).\mathrm{unbot}$.

WithBot.instPredOrder instance

: PredOrder (WithBot α)

Full source

instance : PredOrder (WithBot α) where
  pred a :=
    match a with
    | ⊥ => ⊥
    | Option.some a => ite (pred a = a) ⊥ (some (pred a))
  pred_le a := by
    obtain - | a := a
    · exact bot_le
    change ite _ _ _ ≤ _
    split_ifs
    · exact bot_le
    · exact coe_le_coe.2 (pred_le a)
  min_of_le_pred {a} ha := by
    cases a with
    | bot => exact isMin_bot
    | coe a =>
      dsimp only at ha
      split_ifs at ha with ha'
      · exact (not_coe_le_bot _ ha).elim
      · rw [coe_le_coe, le_pred_iff_isMin, ← pred_eq_iff_isMin] at ha
        exact (ha' ha).elim
  le_pred_of_lt {a b} h := by
    cases a
    · exact bot_le
    cases b
    · exact (not_lt_bot h).elim
    rw [coe_lt_coe] at h
    change _ ≤ ite _ _ _
    split_ifs with hb
    · rw [pred_eq_iff_isMin] at hb
      exact (hb.not_lt h).elim
    · exact coe_le_coe.2 (le_pred_of_lt h)

Predecessor Order Structure on $\mathrm{WithBot}~\alpha$

Informal description

For any preorder $\alpha$ equipped with a predecessor order structure, the type $\mathrm{WithBot}~\alpha$ (obtained by adjoining a least element $\bot$ to $\alpha$) inherits a predecessor order structure. The predecessor function is defined as: - For $\bot$, $\mathrm{pred}(\bot) = \bot$. - For $a \in \alpha$ that is minimal, $\mathrm{pred}(a) = \bot$. - For $a \in \alpha$ that is not minimal, $\mathrm{pred}(a) = \mathrm{pred}_{\alpha}(a)$ (the predecessor in $\alpha$).

WithBot.pred_coe_of_isMin theorem

{a : α} (h : IsMin a) : pred ↑a = (⊥ : WithBot α)

Full source

@[simp]
theorem pred_coe_of_isMin {a : α} (h : IsMin a) : pred ↑a = (⊥ : WithBot α) :=
  dif_pos (pred_eq_iff_isMin.2 h)

Predecessor of Minimal Element in $\mathrm{WithBot}~\alpha$ is $\bot$

Informal description

For any minimal element $a$ in a preorder $\alpha$ equipped with a predecessor function, the predecessor of $a$ in $\mathrm{WithBot}~\alpha$ (where $\bot$ is adjoined as the least element) is $\bot$. That is, $\mathrm{pred}(a) = \bot$.

WithBot.pred_coe_of_not_isMin theorem

{a : α} (h : ¬IsMin a) : pred (↑a : WithBot α) = ↑(pred a)

Full source

theorem pred_coe_of_not_isMin {a : α} (h : ¬ IsMin a) : pred (↑a : WithBot α) = ↑(pred a) :=
  dif_neg (pred_eq_iff_isMin.not.2 h)

Predecessor of Non-Minimal Element in $\mathrm{WithBot}~\alpha$

Informal description

For any element $a$ in a preorder $\alpha$ that is not minimal, the predecessor of the image of $a$ in $\mathrm{WithBot}~\alpha$ is equal to the image of the predecessor of $a$ in $\alpha$. In other words, if $a$ is not minimal, then $\mathrm{pred}(a) = \mathrm{pred}_{\alpha}(a)$ when viewed in $\mathrm{WithBot}~\alpha$.

WithBot.pred_coe theorem

[NoMinOrder α] {a : α} : pred (↑a : WithBot α) = ↑(pred a)

Full source

theorem pred_coe [NoMinOrder α] {a : α} : pred (↑a : WithBot α) = ↑(pred a) :=
  pred_coe_of_not_isMin <| not_isMin a

Predecessor of Element in $\mathrm{WithBot}~\alpha$ for NoMinOrder $\alpha$

Informal description

For any element $a$ in a preorder $\alpha$ with no minimal elements, the predecessor of the image of $a$ in $\mathrm{WithBot}~\alpha$ is equal to the image of the predecessor of $a$ in $\alpha$. That is, $\mathrm{pred}(a) = \mathrm{pred}_{\alpha}(a)$ when viewed in $\mathrm{WithBot}~\alpha$.

WithBot.instIsEmptySuccOrderOfNonempty instance

[hα : Nonempty α] : IsEmpty (SuccOrder (WithBot α))

Full source

instance [hα : Nonempty α] : IsEmpty (SuccOrder (WithBot α)) :=
  ⟨by
    intro
    cases h : succ (⊥ : WithBot α) with
    | bot => exact hα.elim fun a => (max_of_succ_le h.le).not_lt <| bot_lt_coe a
    | coe a =>
      obtain ⟨c, hc⟩ := exists_lt a
      rw [← coe_lt_coe, ← h] at hc
      exact (succ_le_of_lt (bot_lt_coe _)).not_lt hc⟩

Non-existence of Successor Order on WithBot for Nonempty Types

Informal description

For any nonempty ordered type $\alpha$, there is no sensible successor order structure on $\alpha$ with an added bottom element (i.e., $\text{WithBot}\ \alpha$ cannot be equipped with a $\text{SuccOrder}$ instance).

SuccOrder.ofOrderIso abbrev

[SuccOrder X] (f : X ≃o Y) : SuccOrder Y

Full source

/-- `SuccOrder` transfers across equivalences between orders. -/
protected abbrev SuccOrder.ofOrderIso [SuccOrder X] (f : X ≃o Y) : SuccOrder Y where
  succ y := f (succ (f.symm y))
  le_succ y := by rw [← map_inv_le_iff f]; exact le_succ (f.symm y)
  max_of_succ_le h := by
    rw [← f.symm.isMax_apply]
    refine max_of_succ_le ?_
    simp [f.le_symm_apply, h]
  succ_le_of_lt h := by rw [← le_map_inv_iff]; exact succ_le_of_lt (by simp [h])

Transfer of Successor Order Structure via Order Isomorphism

Informal description

Given an order isomorphism $f : X \to Y$ between preorders $X$ and $Y$, if $X$ is equipped with a successor order structure, then $Y$ inherits a successor order structure where the successor of an element $y \in Y$ is defined as $f(\text{succ}(f^{-1}(y)))$.

Set.OrdConnected.predOrder instance

[PredOrder α] : PredOrder s

Full source

noncomputable instance Set.OrdConnected.predOrder [PredOrder α] :
    PredOrder s where
  pred x := if h : Order.pred x.1 ∈ s then ⟨Order.pred x.1, h⟩ else x
  pred_le := fun ⟨x, hx⟩ ↦ by dsimp; split <;> simp_all [Order.pred_le]
  min_of_le_pred := @fun ⟨x, hx⟩ h ↦ by
    dsimp at h
    split_ifs at h with h'
    · simp only [Subtype.mk_le_mk, Order.le_pred_iff_isMin] at h
      rintro ⟨y, _⟩ hy
      simp [h hy]
    · rintro ⟨y, hy⟩ h
      rcases h.lt_or_eq with h | h
      · simp only [Subtype.mk_lt_mk] at h
        have := h.le_pred
        absurd h'
        apply out' hy hx
        simp [this, Order.pred_le]
      · simp [h]
  le_pred_of_lt := @fun ⟨b, hb⟩ ⟨c, hc⟩ h ↦ by
    rw [Subtype.mk_lt_mk] at h
    dsimp only
    split
    · exact h.le_pred
    · exact h.le

Predecessor Order on Order-Connected Subsets

Informal description

For any subset $s$ of a preorder $\alpha$ equipped with a predecessor function, if $s$ is order-connected (i.e., for any $x, y \in s$, the interval $[x, y]$ is contained in $s$), then $s$ inherits a predecessor order structure where the predecessor of an element in $s$ is its predecessor in $\alpha$ when it lies in $s$, and otherwise the element is minimal in $s$.

coe_pred_of_mem theorem

[PredOrder α] {a : s} (h : pred a.1 ∈ s) : (pred a).1 = pred ↑a

Full source

@[simp, norm_cast]
lemma coe_pred_of_mem [PredOrder α] {a : s} (h : predpred a.1 ∈ s) :
    (pred a).1 = pred ↑a := by classical
  change Subtype.val (dite ..) = _
  simp [h]

Agreement of Predecessor Function on Order-Connected Subsets

Informal description

Let $\alpha$ be a preorder equipped with a predecessor function $\mathrm{pred} : \alpha \to \alpha$, and let $s$ be an order-connected subset of $\alpha$. For any element $a \in s$ such that $\mathrm{pred}(a) \in s$, the predecessor of $a$ in $s$ (denoted $\mathrm{pred}(a)$) coincides with the predecessor of $a$ in $\alpha$ (denoted $\mathrm{pred}(a)$). In other words, the predecessor operation in $s$ agrees with the restriction of the predecessor operation from $\alpha$ to $s$ when the predecessor lies within $s$.

isMin_of_not_pred_mem theorem

[PredOrder α] {a : s} (h : pred ↑a ∉ s) : IsMin a

Full source

lemma isMin_of_not_pred_mem [PredOrder α] {a : s} (h : predpred ↑a ∉ s) : IsMin a := by classical
  rw [← pred_eq_iff_isMin]
  change dite .. = _
  simp [h]

Minimality from Absence of Predecessor in Order-Connected Subset

Informal description

Let $\alpha$ be a preorder equipped with a predecessor function $\mathrm{pred} : \alpha \to \alpha$, and let $s$ be an order-connected subset of $\alpha$. For any element $a \in s$, if the predecessor of $a$ in $\alpha$ does not belong to $s$, then $a$ is a minimal element in $s$.

not_pred_mem_iff_isMin theorem

[PredOrder α] [NoMinOrder α] {a : s} : pred ↑a ∉ s ↔ IsMin a

Full source

lemma not_pred_mem_iff_isMin [PredOrder α] [NoMinOrder α] {a : s} :
    predpred ↑a ∉ spred ↑a ∉ s ↔ IsMin a where
  mp := isMin_of_not_pred_mem
  mpr h nh := by
    replace h := congr($h.pred_eq.1)
    rw [coe_pred_of_mem nh] at h
    simp at h

Characterization of Minimal Elements via Predecessor Absence in Order-Connected Subsets

Informal description

Let $\alpha$ be a preorder equipped with a predecessor function $\mathrm{pred} \colon \alpha \to \alpha$ and no minimal elements, and let $s$ be an order-connected subset of $\alpha$. For any element $a \in s$, the predecessor of $a$ in $\alpha$ does not belong to $s$ if and only if $a$ is a minimal element in $s$.

Set.OrdConnected.succOrder instance

[SuccOrder α] : SuccOrder s

Full source

noncomputable instance Set.OrdConnected.succOrder [SuccOrder α] :
    SuccOrder s :=
  letI : PredOrder sᵒᵈ := inferInstanceAs (PredOrder (OrderDual.ofDualOrderDual.ofDual ⁻¹' s))
  inferInstanceAs (SuccOrder sᵒᵈsᵒᵈᵒᵈ)

Successor Order on Order-Connected Subsets

Informal description

For any subset $s$ of a preorder $\alpha$ equipped with a successor function, if $s$ is order-connected (i.e., for any $x, y \in s$, the interval $[x, y]$ is contained in $s$), then $s$ inherits a successor order structure where the successor of an element in $s$ is its successor in $\alpha$ when it lies in $s$, and otherwise the element is maximal in $s$.

coe_succ_of_mem theorem

[SuccOrder α] {a : s} (h : succ ↑a ∈ s) : (succ a).1 = succ ↑a

Full source

@[simp, norm_cast]
lemma coe_succ_of_mem [SuccOrder α] {a : s} (h : succsucc ↑a ∈ s) :
    (succ a).1 = succ ↑a := by classical
  change Subtype.val (dite ..) = _
  split_ifs <;> trivial

Successor Projection Equality in Order-Connected Subsets

Informal description

Let $\alpha$ be a preorder equipped with a successor order structure, and let $s$ be a subset of $\alpha$. For any element $a \in s$ such that the successor of $a$ in $\alpha$ (denoted $\mathrm{succ}(a)$) is also in $s$, the first projection of the successor of $a$ in $s$ is equal to the successor of $a$ in $\alpha$, i.e., $(\mathrm{succ}(a)).1 = \mathrm{succ}(a)$.

isMax_of_not_succ_mem theorem

[SuccOrder α] {a : s} (h : succ ↑a ∉ s) : IsMax a

Full source

lemma isMax_of_not_succ_mem [SuccOrder α] {a : s} (h : succsucc ↑a ∉ s) : IsMax a := by classical
  rw [← succ_eq_iff_isMax]
  change dite .. = _
  split_ifs <;> trivial

Maximality from Non-Membership of Successor in Order-Connected Subsets

Informal description

Let $\alpha$ be a preorder equipped with a successor function, and let $s$ be an order-connected subset of $\alpha$. For any element $a \in s$, if the successor of $a$ (in $\alpha$) does not belong to $s$, then $a$ is a maximal element of $s$.

not_succ_mem_iff_isMax theorem

[SuccOrder α] [NoMaxOrder α] {a : s} : succ ↑a ∉ s ↔ IsMax a

Full source

lemma not_succ_mem_iff_isMax [SuccOrder α] [NoMaxOrder α] {a : s} :
    succsucc ↑a ∉ ssucc ↑a ∉ s ↔ IsMax a where
  mp := isMax_of_not_succ_mem
  mpr h nh := by
    replace h := congr($h.succ_eq.1)
    rw [coe_succ_of_mem nh] at h
    simp at h

Non-Membership of Successor in Order-Connected Subset Characterizes Maximal Elements in NoMaxOrder

Informal description

Let $\alpha$ be a preorder equipped with a successor function, and let $s$ be an order-connected subset of $\alpha$ where $\alpha$ has no maximal elements. For any element $a \in s$, the successor of $a$ in $\alpha$ does not belong to $s$ if and only if $a$ is a maximal element of $s$.

Mathlib.Order.SuccPred.Basic

Typeclasses

Implementation notes