doc-next-gen

Mathlib.Order.SuccPred.Limit

Module docstring

{"# Successor and predecessor limits

We define the predicate Order.IsSuccPrelimit for \"successor pre-limits\", values that don't cover any others. They are so named since they can't be the successors of anything smaller. We define Order.IsPredPrelimit analogously, and prove basic results.

For some applications, it is desirable to exclude minimal elements from being successor limits, or maximal elements from being predecessor limits. As such, we also provide Order.IsSuccLimit and Order.IsPredLimit, which exclude these cases.

TODO

The plan is to eventually replace Ordinal.IsLimit and Cardinal.IsLimit with the common predicate Order.IsSuccLimit. ","### Successor limits ","### Predecessor limits ","### Induction principles "}

Order.IsSuccPrelimit definition
(a : α) : Prop
Full source 
/-- A successor pre-limit is a value that doesn't cover any other.

It's so named because in a successor order, a successor pre-limit can't be the successor of anything
smaller.

Use `IsSuccLimit` if you want to exclude the case of a minimal element. -/
def IsSuccPrelimit (a : α) : Prop :=
  ∀ b, ¬b ⋖ a
Successor pre-limit element in a partial order
Informal description
An element $a$ in a partially ordered set $\alpha$ is called a *successor pre-limit* if there does not exist any element $b$ that is covered by $a$ (i.e., there is no $b$ such that $b \lessdot a$). This means that $a$ cannot be the immediate successor of any other element in the order.
Order.not_isSuccPrelimit_iff_exists_covBy theorem
(a : α) : ¬IsSuccPrelimit a ↔ ∃ b, b ⋖ a
Full source 
theorem not_isSuccPrelimit_iff_exists_covBy (a : α) : ¬IsSuccPrelimit a¬IsSuccPrelimit a ↔ ∃ b, b ⋖ a := by
  simp [IsSuccPrelimit]
Characterization of Non-Successor-Prelimit Elements via Covering Relation
Informal description
An element $a$ in a partially ordered set $\alpha$ is *not* a successor pre-limit if and only if there exists an element $b$ such that $b$ is covered by $a$ (i.e., $b \lessdot a$).
Order.IsSuccPrelimit.of_dense theorem
[DenselyOrdered α] (a : α) : IsSuccPrelimit a
Full source 
@[simp]
theorem IsSuccPrelimit.of_dense [DenselyOrdered α] (a : α) : IsSuccPrelimit a := fun _ => not_covBy
Every Element is a Successor Pre-Limit in a Densely Ordered Set
Informal description
In a densely ordered set $\alpha$, every element $a$ is a successor pre-limit, meaning there does not exist any element $b$ such that $b$ is covered by $a$ (i.e., $b \lessdot a$).
Order.IsSuccLimit definition
(a : α) : Prop
Full source 
/-- A successor limit is a value that isn't minimal and doesn't cover any other.

It's so named because in a successor order, a successor limit can't be the successor of anything
smaller.

This previously allowed the element to be minimal. This usage is now covered by `IsSuccPrelimit`. -/
def IsSuccLimit (a : α) : Prop :=
  ¬ IsMin a¬ IsMin a ∧ IsSuccPrelimit a
Successor limit element in a partial order
Informal description
An element $a$ in a partially ordered set $\alpha$ is called a *successor limit* if it is not a minimal element and does not cover any other element (i.e., there is no $b$ such that $b \lessdot a$). This means that $a$ cannot be the immediate successor of any other element in the order and is not minimal.
Order.IsSuccLimit.not_isMin theorem
(h : IsSuccLimit a) : ¬IsMin a
Full source 
protected theorem IsSuccLimit.not_isMin (h : IsSuccLimit a) : ¬ IsMin a := h.1
Successor limits are non-minimal elements
Informal description
If an element $a$ in a partially ordered set is a successor limit, then $a$ is not a minimal element.
Order.IsSuccLimit.isSuccPrelimit theorem
(h : IsSuccLimit a) : IsSuccPrelimit a
Full source 
protected theorem IsSuccLimit.isSuccPrelimit (h : IsSuccLimit a) : IsSuccPrelimit a := h.2
Successor limits are successor pre-limits
Informal description
If an element $a$ in a partially ordered set is a successor limit, then $a$ is also a successor pre-limit.
Order.IsSuccPrelimit.isSuccLimit_of_not_isMin theorem
(h : IsSuccPrelimit a) (ha : ¬IsMin a) : IsSuccLimit a
Full source 
theorem IsSuccPrelimit.isSuccLimit_of_not_isMin (h : IsSuccPrelimit a) (ha : ¬ IsMin a) :
    IsSuccLimit a :=
  ⟨ha, h⟩
Characterization of successor limits via successor pre-limits and non-minimality
Informal description
For any element $a$ in a partially ordered set, if $a$ is a successor pre-limit and $a$ is not minimal, then $a$ is a successor limit.
Order.IsSuccPrelimit.isSuccLimit theorem
[NoMinOrder α] (h : IsSuccPrelimit a) : IsSuccLimit a
Full source 
theorem IsSuccPrelimit.isSuccLimit [NoMinOrder α] (h : IsSuccPrelimit a) : IsSuccLimit a :=
  h.isSuccLimit_of_not_isMin (not_isMin a)
Successor pre-limits are successor limits in NoMinOrder
Informal description
In a partially ordered set $\alpha$ with no minimal elements, if an element $a$ is a successor pre-limit (i.e., there is no element $b$ such that $b$ is covered by $a$), then $a$ is a successor limit (i.e., $a$ is not minimal and does not cover any other element).
Order.isSuccPrelimit_iff_isSuccLimit_of_not_isMin theorem
(h : ¬IsMin a) : IsSuccPrelimit a ↔ IsSuccLimit a
Full source 
theorem isSuccPrelimit_iff_isSuccLimit_of_not_isMin (h : ¬ IsMin a) :
    IsSuccPrelimitIsSuccPrelimit a ↔ IsSuccLimit a :=
  ⟨fun ha ↦ ha.isSuccLimit_of_not_isMin h, IsSuccLimit.isSuccPrelimit⟩
Characterization of successor limits for non-minimal elements: $a$ is a successor pre-limit $\iff$ $a$ is a successor limit
Informal description
For an element $a$ in a partially ordered set that is not minimal, $a$ is a successor pre-limit if and only if $a$ is a successor limit. Here: - A *successor pre-limit* means there is no element $b$ such that $b$ is covered by $a$ (i.e., no $b \lessdot a$). - A *successor limit* means $a$ is not minimal and there is no element $b$ such that $b \lessdot a$.
Order.isSuccPrelimit_iff_isSuccLimit theorem
[NoMinOrder α] : IsSuccPrelimit a ↔ IsSuccLimit a
Full source 
theorem isSuccPrelimit_iff_isSuccLimit [NoMinOrder α] : IsSuccPrelimitIsSuccPrelimit a ↔ IsSuccLimit a :=
  isSuccPrelimit_iff_isSuccLimit_of_not_isMin (not_isMin a)
Equivalence of Successor Pre-Limits and Successor Limits in NoMinOrder
Informal description
In a partially ordered set $\alpha$ with no minimal elements, an element $a$ is a successor pre-limit if and only if it is a successor limit. Here: - A *successor pre-limit* means there is no element $b$ such that $b$ is covered by $a$ (i.e., no $b \lessdot a$). - A *successor limit* means $a$ is not minimal and there is no element $b$ such that $b \lessdot a$.
IsMin.not_isSuccLimit theorem
(h : IsMin a) : ¬IsSuccLimit a
Full source 
protected theorem _root_.IsMin.not_isSuccLimit (h : IsMin a) : ¬ IsSuccLimit a :=
  fun ha ↦ ha.not_isMin h
Minimal elements are not successor limits
Informal description
If an element $a$ in a partially ordered set is minimal, then $a$ is not a successor limit.
IsMin.isSuccPrelimit theorem
: IsMin a → IsSuccPrelimit a
Full source 
protected theorem _root_.IsMin.isSuccPrelimit : IsMin a → IsSuccPrelimit a := fun h _ hab =>
  not_isMin_of_lt hab.lt h
Minimal Elements are Successor Pre-Limits
Informal description
If an element $a$ in a partially ordered set is minimal (i.e., there is no element strictly less than $a$), then $a$ is a successor pre-limit (i.e., there is no element covered by $a$).
Order.isSuccPrelimit_bot theorem
[OrderBot α] : IsSuccPrelimit (⊥ : α)
Full source 
theorem isSuccPrelimit_bot [OrderBot α] : IsSuccPrelimit (⊥ : α) :=
  isMin_bot.isSuccPrelimit
Bottom Element is a Successor Pre-Limit
Informal description
In a partially ordered set $\alpha$ with a bottom element $\bot$, the bottom element is a successor pre-limit, meaning there is no element covered by $\bot$.
Order.IsSuccLimit.ne_bot theorem
[OrderBot α] (h : IsSuccLimit a) : a ≠ ⊥
Full source 
theorem IsSuccLimit.ne_bot [OrderBot α] (h : IsSuccLimit a) : a ≠ ⊥ := by
  rintro rfl
  exact not_isSuccLimit_bot h
Successor Limit Elements are Not Bottom
Informal description
In a partially ordered set $\alpha$ with a bottom element $\bot$, if an element $a$ is a successor limit, then $a$ is not equal to $\bot$.
Order.not_isSuccLimit_iff theorem
: ¬IsSuccLimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a
Full source 
theorem not_isSuccLimit_iff : ¬ IsSuccLimit a¬ IsSuccLimit a ↔ IsMin a ∨ ¬ IsSuccPrelimit a := by
  rw [IsSuccLimit, not_and_or, not_not]
Characterization of Non-Successor Limit Elements
Informal description
An element $a$ in a partially ordered set is not a successor limit if and only if $a$ is a minimal element or $a$ is not a successor pre-limit. In other words, $\neg \text{IsSuccLimit}(a) \leftrightarrow \text{IsMin}(a) \lor \neg \text{IsSuccPrelimit}(a)$.
Order.IsSuccPrelimit.isMax theorem
(h : IsSuccPrelimit (succ a)) : IsMax a
Full source 
protected theorem IsSuccPrelimit.isMax (h : IsSuccPrelimit (succ a)) : IsMax a := by
  by_contra H
  exact h a (covBy_succ_of_not_isMax H)
Maximality from Successor Pre-Limit Condition
Informal description
If the successor of an element $a$ in a partially ordered set is a successor pre-limit, then $a$ is a maximal element.
Order.IsSuccLimit.isMax theorem
(h : IsSuccLimit (succ a)) : IsMax a
Full source 
protected theorem IsSuccLimit.isMax (h : IsSuccLimit (succ a)) : IsMax a :=
  h.isSuccPrelimit.isMax
Maximality from Successor Limit Condition
Informal description
If the successor of an element $a$ in a partially ordered set is a successor limit, then $a$ is a maximal element.
Order.not_isSuccPrelimit_succ_of_not_isMax theorem
(ha : ¬IsMax a) : ¬IsSuccPrelimit (succ a)
Full source 
theorem not_isSuccPrelimit_succ_of_not_isMax (ha : ¬ IsMax a) : ¬ IsSuccPrelimit (succ a) :=
  mt IsSuccPrelimit.isMax ha
Non-maximal elements have successors that are not pre-limits
Informal description
For any element $a$ in a partially ordered set $\alpha$ that is not maximal, the successor of $a$ is not a successor pre-limit. In other words, if $a$ is not maximal, then there exists some element $b$ such that $b \lessdot \text{succ}(a)$.
Order.not_isSuccLimit_succ_of_not_isMax theorem
(ha : ¬IsMax a) : ¬IsSuccLimit (succ a)
Full source 
theorem not_isSuccLimit_succ_of_not_isMax (ha : ¬ IsMax a) : ¬ IsSuccLimit (succ a) :=
  mt IsSuccLimit.isMax ha
Non-maximal elements have successors that are not successor limits
Informal description
For any element $a$ in a partially ordered set $\alpha$, if $a$ is not maximal, then the successor of $a$ is not a successor limit.
Order.IsSuccPrelimit.mid definition
{i j : α} (hi : IsSuccPrelimit i) (hj : j < i) : Ioo j i
Full source 
/-- Given `j < i` with `i` a prelimit, `IsSuccPrelimit.mid` picks an arbitrary element strictly
between `j` and `i`. -/
noncomputable def IsSuccPrelimit.mid {i j : α} (hi : IsSuccPrelimit i) (hj : j < i) :
    Ioo j i :=
  Classical.indefiniteDescription _ ((not_covBy_iff hj).mp <| hi j)
Intermediate element between a successor pre-limit and a smaller element
Informal description
Given an element $i$ in a partial order $\alpha$ that is a successor pre-limit (i.e., $i$ does not cover any other element) and an element $j < i$, the function `IsSuccPrelimit.mid` selects an arbitrary element strictly between $j$ and $i$ (i.e., an element in the open interval $(j, i)$).
Order.IsSuccPrelimit.succ_ne theorem
(h : IsSuccPrelimit a) (b : α) : succ b ≠ a
Full source 
theorem IsSuccPrelimit.succ_ne (h : IsSuccPrelimit a) (b : α) : succsucc b ≠ a := by
  rintro rfl
  exact not_isMax _ h.isMax
Successor Pre-Limit Implies No Element Has Successor Equal to It
Informal description
For any element $a$ in a partially ordered set $\alpha$, if $a$ is a successor pre-limit (i.e., there is no element covered by $a$), then for any element $b \in \alpha$, the successor of $b$ is not equal to $a$.
Order.IsSuccLimit.succ_ne theorem
(h : IsSuccLimit a) (b : α) : succ b ≠ a
Full source 
theorem IsSuccLimit.succ_ne (h : IsSuccLimit a) (b : α) : succsucc b ≠ a :=
  h.isSuccPrelimit.succ_ne b
No Element Has Successor Equal to a Successor Limit
Informal description
For any element $a$ in a partially ordered set $\alpha$, if $a$ is a successor limit (i.e., $a$ is not minimal and does not cover any other element), then for any element $b \in \alpha$, the successor of $b$ is not equal to $a$.
Order.not_isSuccPrelimit_succ theorem
(a : α) : ¬IsSuccPrelimit (succ a)
Full source 
@[simp]
theorem not_isSuccPrelimit_succ (a : α) : ¬IsSuccPrelimit (succ a) := fun h => h.succ_ne _ rfl
Successor of Any Element is Not a Successor Pre-Limit
Informal description
For any element $a$ in a partially ordered set $\alpha$ equipped with a successor function, the successor of $a$ is not a successor pre-limit element. That is, $\text{succ}(a)$ cannot be an element that doesn't cover any other elements.
Order.not_isSuccLimit_succ theorem
(a : α) : ¬IsSuccLimit (succ a)
Full source 
@[simp]
theorem not_isSuccLimit_succ (a : α) : ¬IsSuccLimit (succ a) := fun h => h.succ_ne _ rfl
Successor of Any Element is Not a Successor Limit
Informal description
For any element $a$ in a partially ordered set $\alpha$ equipped with a successor function, the successor of $a$ is not a successor limit element. That is, $\text{succ}(a)$ cannot be an element that is both non-minimal and does not cover any other elements.
Order.IsSuccPrelimit.isMin_of_noMax theorem
(h : IsSuccPrelimit a) : IsMin a
Full source 
theorem IsSuccPrelimit.isMin_of_noMax (h : IsSuccPrelimit a) : IsMin a := by
  intro b hb
  rcases hb.exists_succ_iterate with ⟨_ | n, rfl⟩
  · exact le_rfl
  · rw [iterate_succ_apply'] at h
    exact (not_isSuccPrelimit_succ _ h).elim
Successor Pre-Limit Implies Minimal Element in Orders Without Maxima
Informal description
If an element $a$ in a partially ordered set $\alpha$ is a successor pre-limit (i.e., it does not cover any other element), and $\alpha$ has no maximal elements, then $a$ is a minimal element of $\alpha$.
Order.not_isSuccPrelimit_of_noMax theorem
[NoMinOrder α] : ¬IsSuccPrelimit a
Full source 
theorem not_isSuccPrelimit_of_noMax [NoMinOrder α] : ¬ IsSuccPrelimit a := by simp
No successor pre-limits in orders without minimal elements
Informal description
In a partial order $\alpha$ with no minimal elements, no element $a \in \alpha$ is a successor pre-limit.
Order.isSuccLimit_iff theorem
[OrderBot α] : IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a
Full source 
theorem isSuccLimit_iff [OrderBot α] : IsSuccLimitIsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a := by
  rw [IsSuccLimit, isMin_iff_eq_bot]
Characterization of Successor Limit Elements in Orders with Bottom
Informal description
Let $\alpha$ be a partially ordered set with a bottom element $\bot$. An element $a \in \alpha$ is a successor limit if and only if $a$ is not equal to $\bot$ and $a$ is a successor pre-limit (i.e., there is no element $b$ such that $b$ is covered by $a$).
Order.IsSuccLimit.bot_lt theorem
[OrderBot α] (h : IsSuccLimit a) : ⊥ < a
Full source 
theorem IsSuccLimit.bot_lt [OrderBot α] (h : IsSuccLimit a) : ⊥ < a :=
  h.ne_bot.bot_lt
Bottom Element is Strictly Below Successor Limit Elements
Informal description
In a partially ordered set $\alpha$ with a bottom element $\bot$, if $a$ is a successor limit element, then $\bot$ is strictly less than $a$, i.e., $\bot < a$.
Order.isSuccPrelimit_of_succ_ne theorem
(h : ∀ b, succ b ≠ a) : IsSuccPrelimit a
Full source 
theorem isSuccPrelimit_of_succ_ne (h : ∀ b, succsucc b ≠ a) : IsSuccPrelimit a := fun b hba =>
  h b (CovBy.succ_eq hba)
Characterization of successor pre-limit elements via successor function
Informal description
For any element $a$ in a partially ordered set $\alpha$ with a successor function, if for every element $b$ the successor of $b$ is not equal to $a$, then $a$ is a successor pre-limit element.
Order.not_isSuccPrelimit_iff theorem
: ¬IsSuccPrelimit a ↔ ∃ b, ¬IsMax b ∧ succ b = a
Full source 
theorem not_isSuccPrelimit_iff : ¬ IsSuccPrelimit a¬ IsSuccPrelimit a ↔ ∃ b, ¬ IsMax b ∧ succ b = a := by
  rw [not_isSuccPrelimit_iff_exists_covBy]
  refine exists_congr fun b => ⟨fun hba => ⟨hba.lt.not_isMax, (CovBy.succ_eq hba)⟩, ?_⟩
  rintro ⟨h, rfl⟩
  exact covBy_succ_of_not_isMax h
Characterization of Non-Successor-Prelimit Elements via Non-Maximal Predecessors
Informal description
An element $a$ in a partially ordered set $\alpha$ is *not* a successor pre-limit if and only if there exists an element $b$ that is not maximal and whose successor is $a$, i.e., $\mathrm{succ}(b) = a$.
Order.mem_range_succ_of_not_isSuccPrelimit theorem
(h : ¬IsSuccPrelimit a) : a ∈ range (succ : α → α)
Full source 
/-- See `not_isSuccPrelimit_iff` for a version that states that `a` is a successor of a value other
than itself. -/
theorem mem_range_succ_of_not_isSuccPrelimit (h : ¬ IsSuccPrelimit a) :
    a ∈ range (succ : α → α) := by
  obtain ⟨b, hb⟩ := not_isSuccPrelimit_iff.1 h
  exact ⟨b, hb.2⟩
Non-Successor-Prelimit Elements Belong to Successor Function's Range
Informal description
For any element $a$ in a partially ordered set $\alpha$ with a successor function, if $a$ is not a successor pre-limit, then $a$ is in the range of the successor function, i.e., there exists some element $b \in \alpha$ such that $\mathrm{succ}(b) = a$.
Order.mem_range_succ_or_isSuccPrelimit theorem
(a) : a ∈ range (succ : α → α) ∨ IsSuccPrelimit a
Full source 
theorem mem_range_succ_or_isSuccPrelimit (a) : a ∈ range (succ : α → α)a ∈ range (succ : α → α) ∨ IsSuccPrelimit a :=
  or_iff_not_imp_right.2 <| mem_range_succ_of_not_isSuccPrelimit
Decomposition of Elements into Successor Images or Successor Pre-Limits
Informal description
For any element $a$ in a partially ordered set $\alpha$ equipped with a successor function $\mathrm{succ}$, either $a$ is in the range of $\mathrm{succ}$ (i.e., there exists some $b \in \alpha$ such that $\mathrm{succ}(b) = a$), or $a$ is a successor pre-limit (i.e., there is no element covered by $a$).
Order.isMin_or_mem_range_succ_or_isSuccLimit theorem
(a) : IsMin a ∨ a ∈ range (succ : α → α) ∨ IsSuccLimit a
Full source 
theorem isMin_or_mem_range_succ_or_isSuccLimit (a) :
    IsMinIsMin a ∨ a ∈ range (succ : α → α) ∨ IsSuccLimit a := by
  rw [IsSuccLimit]
  have := mem_range_succ_or_isSuccPrelimit a
  tauto
Decomposition of Elements into Minimal, Successor Images, or Successor Limits
Informal description
For any element $a$ in a partially ordered set $\alpha$ equipped with a successor function $\mathrm{succ}$, either: 1. $a$ is a minimal element, or 2. $a$ is in the range of $\mathrm{succ}$ (i.e., there exists some $b \in \alpha$ such that $\mathrm{succ}(b) = a$), or 3. $a$ is a successor limit (i.e., $a$ is not minimal and does not cover any other element).
Order.isSuccPrelimit_of_succ_lt theorem
(H : ∀ a < b, succ a < b) : IsSuccPrelimit b
Full source 
theorem isSuccPrelimit_of_succ_lt (H : ∀ a < b, succ a < b) : IsSuccPrelimit b := fun a hab =>
  (H a hab.lt).ne (CovBy.succ_eq hab)
Sufficient Condition for Successor Pre-Limit Element: $\forall a < b, \text{succ}(a) < b$ implies $b$ is a successor pre-limit
Informal description
Let $\alpha$ be a preorder equipped with a successor function $\text{succ}$. If for every element $a < b$ in $\alpha$, the successor $\text{succ}(a) < b$, then $b$ is a successor pre-limit element (i.e., there is no element covered by $b$).
Order.IsSuccPrelimit.succ_lt theorem
(hb : IsSuccPrelimit b) (ha : a < b) : succ a < b
Full source 
theorem IsSuccPrelimit.succ_lt (hb : IsSuccPrelimit b) (ha : a < b) : succ a < b := by
  by_cases h : IsMax a
  · rwa [h.succ_eq]
  · rw [lt_iff_le_and_ne, succ_le_iff_of_not_isMax h]
    refine ⟨ha, fun hab => ?_⟩
    subst hab
    exact (h hb.isMax).elim
Successor Pre-Limit Implies $\text{succ}(a) < b$ for $a < b$
Informal description
Let $a$ and $b$ be elements of a partially ordered set $\alpha$ equipped with a successor function $\text{succ}$. If $b$ is a successor pre-limit (i.e., there is no element covered by $b$) and $a < b$, then the successor of $a$ is strictly less than $b$, i.e., $\text{succ}(a) < b$.
Order.IsSuccLimit.succ_lt theorem
(hb : IsSuccLimit b) (ha : a < b) : succ a < b
Full source 
theorem IsSuccLimit.succ_lt (hb : IsSuccLimit b) (ha : a < b) : succ a < b :=
  hb.isSuccPrelimit.succ_lt ha
Successor Limit Implies $\text{succ}(a) < b$ for $a < b$
Informal description
Let $\alpha$ be a partially ordered set equipped with a successor function $\text{succ}$. If $b$ is a successor limit element (i.e., $b$ is not minimal and does not cover any other element) and $a < b$, then the successor of $a$ is strictly less than $b$, i.e., $\text{succ}(a) < b$.
Order.IsSuccPrelimit.succ_lt_iff theorem
(hb : IsSuccPrelimit b) : succ a < b ↔ a < b
Full source 
theorem IsSuccPrelimit.succ_lt_iff (hb : IsSuccPrelimit b) : succsucc a < b ↔ a < b :=
  ⟨fun h => (le_succ a).trans_lt h, hb.succ_lt⟩
Equivalence of Successor Inequality and Element Inequality for Successor Pre-Limits
Informal description
Let $b$ be a successor pre-limit element in a partially ordered set $\alpha$ equipped with a successor function $\text{succ}$. Then for any element $a \in \alpha$, the inequality $\text{succ}(a) < b$ holds if and only if $a < b$.
Order.IsSuccLimit.succ_lt_iff theorem
(hb : IsSuccLimit b) : succ a < b ↔ a < b
Full source 
theorem IsSuccLimit.succ_lt_iff (hb : IsSuccLimit b) : succsucc a < b ↔ a < b :=
  hb.isSuccPrelimit.succ_lt_iff
Equivalence of Successor Inequality and Element Inequality for Successor Limits
Informal description
Let $\alpha$ be a partially ordered set equipped with a successor function $\text{succ}$. For any successor limit element $b \in \alpha$ (i.e., $b$ is not minimal and does not cover any other element), the inequality $\text{succ}(a) < b$ holds if and only if $a < b$.
Order.isSuccPrelimit_iff_succ_lt theorem
: IsSuccPrelimit b ↔ ∀ a < b, succ a < b
Full source 
theorem isSuccPrelimit_iff_succ_lt : IsSuccPrelimitIsSuccPrelimit b ↔ ∀ a < b, succ a < b :=
  ⟨fun hb _ => hb.succ_lt, isSuccPrelimit_of_succ_lt⟩
Characterization of Successor Pre-Limit Elements via Successor Inequality
Informal description
An element $b$ in a preorder $\alpha$ equipped with a successor function $\text{succ}$ is a successor pre-limit if and only if for every element $a < b$, the successor $\text{succ}(a) < b$.
Order.isSuccPrelimit_iff_succ_ne theorem
: IsSuccPrelimit a ↔ ∀ b, succ b ≠ a
Full source 
theorem isSuccPrelimit_iff_succ_ne : IsSuccPrelimitIsSuccPrelimit a ↔ ∀ b, succ b ≠ a :=
  ⟨IsSuccPrelimit.succ_ne, isSuccPrelimit_of_succ_ne⟩
Characterization of Successor Pre-Limit Elements via Successor Function
Informal description
An element $a$ in a partially ordered set $\alpha$ with a successor function is a successor pre-limit if and only if for every element $b \in \alpha$, the successor of $b$ is not equal to $a$.
Order.not_isSuccPrelimit_iff' theorem
: ¬IsSuccPrelimit a ↔ a ∈ range (succ : α → α)
Full source 
theorem not_isSuccPrelimit_iff' : ¬ IsSuccPrelimit a¬ IsSuccPrelimit a ↔ a ∈ range (succ : α → α) := by
  simp_rw [isSuccPrelimit_iff_succ_ne, not_forall, not_ne_iff, mem_range]
Characterization of Non-Successor-Prelimit Elements via Successor Function Range
Informal description
An element $a$ in a partially ordered set $\alpha$ is *not* a successor pre-limit if and only if $a$ is in the range of the successor function, i.e., there exists some element $b \in \alpha$ such that $a = \text{succ}(b)$.
Order.IsSuccPrelimit.isMin theorem
(h : IsSuccPrelimit a) : IsMin a
Full source 
protected theorem IsSuccPrelimit.isMin (h : IsSuccPrelimit a) : IsMin a := fun b hb => by
  revert h
  refine Succ.rec (fun _ => le_rfl) (fun c _ H hc => ?_) hb
  have := hc.isMax.succ_eq
  rw [this] at hc ⊢
  exact H hc
Successor Prelimit Implies Minimal Element
Informal description
If an element $a$ in a partially ordered set is a successor pre-limit (i.e., there is no element $b$ such that $b$ is covered by $a$), then $a$ is a minimal element.
Order.isSuccPrelimit_iff theorem
: IsSuccPrelimit a ↔ IsMin a
Full source 
@[simp]
theorem isSuccPrelimit_iff : IsSuccPrelimitIsSuccPrelimit a ↔ IsMin a :=
  ⟨IsSuccPrelimit.isMin, IsMin.isSuccPrelimit⟩
Characterization of Successor Pre-Limits as Minimal Elements
Informal description
An element $a$ in a partially ordered set is a successor pre-limit if and only if it is a minimal element. In other words, $a$ does not cover any other element precisely when there is no element strictly less than $a$.
Order.not_isSuccPrelimit theorem
[NoMinOrder α] : ¬IsSuccPrelimit a
Full source 
theorem not_isSuccPrelimit [NoMinOrder α] : ¬ IsSuccPrelimit a := by simp
Nonexistence of Successor Pre-Limits in No-Min-Order Posets
Informal description
In a partially ordered set $\alpha$ with no minimal elements, no element $a \in \alpha$ is a successor pre-limit.
Order.IsSuccPrelimit.le_iff_forall_le theorem
(h : IsSuccPrelimit a) : a ≤ b ↔ ∀ c < a, c ≤ b
Full source 
theorem IsSuccPrelimit.le_iff_forall_le (h : IsSuccPrelimit a) : a ≤ b ↔ ∀ c < a, c ≤ b := by
  use fun ha c hc ↦ hc.le.trans ha
  intro H
  by_contra! ha
  exact h b ⟨ha, fun c hb hc ↦ (H c hc).not_lt hb⟩
Characterization of Order Relation for Successor Pre-Limit Elements
Informal description
Let $a$ be a successor pre-limit element in a partially ordered set $\alpha$. Then for any element $b \in \alpha$, we have $a \leq b$ if and only if every element $c < a$ satisfies $c \leq b$.
Order.IsSuccLimit.le_iff_forall_le theorem
(h : IsSuccLimit a) : a ≤ b ↔ ∀ c < a, c ≤ b
Full source 
theorem IsSuccLimit.le_iff_forall_le (h : IsSuccLimit a) : a ≤ b ↔ ∀ c < a, c ≤ b :=
  h.isSuccPrelimit.le_iff_forall_le
Characterization of Order Relation for Successor Limit Elements
Informal description
Let $a$ be a successor limit element in a partially ordered set $\alpha$. Then for any element $b \in \alpha$, we have $a \leq b$ if and only if every element $c < a$ satisfies $c \leq b$.
Order.IsSuccPrelimit.lt_iff_exists_lt theorem
(h : IsSuccPrelimit b) : a < b ↔ ∃ c < b, a < c
Full source 
theorem IsSuccPrelimit.lt_iff_exists_lt (h : IsSuccPrelimit b) : a < b ↔ ∃ c < b, a < c := by
  rw [← not_iff_not]
  simp [h.le_iff_forall_le]
Characterization of Strict Order Relation for Successor Pre-Limit Elements
Informal description
Let $b$ be a successor pre-limit element in a partially ordered set $\alpha$. Then for any element $a \in \alpha$, we have $a < b$ if and only if there exists an element $c < b$ such that $a < c$.
Order.IsSuccLimit.lt_iff_exists_lt theorem
(h : IsSuccLimit b) : a < b ↔ ∃ c < b, a < c
Full source 
theorem IsSuccLimit.lt_iff_exists_lt (h : IsSuccLimit b) : a < b ↔ ∃ c < b, a < c :=
  h.isSuccPrelimit.lt_iff_exists_lt
Characterization of Strict Order Relation for Successor Limit Elements
Informal description
Let $b$ be a successor limit element in a partially ordered set $\alpha$. Then for any element $a \in \alpha$, the relation $a < b$ holds if and only if there exists an element $c < b$ such that $a < c$.
IsLUB.isSuccPrelimit_of_not_mem theorem
{s : Set α} (hs : IsLUB s a) (ha : a ∉ s) : IsSuccPrelimit a
Full source 
lemma _root_.IsLUB.isSuccPrelimit_of_not_mem {s : Set α} (hs : IsLUB s a) (ha : a ∉ s) :
    IsSuccPrelimit a := by
  intro b hb
  obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt
  obtain rfl := (hb.ge_of_gt hbc).antisymm hca
  contradiction
Least upper bound outside set is successor pre-limit
Informal description
Let $\alpha$ be a partially ordered set, $s \subseteq \alpha$ a subset, and $a \in \alpha$ an element. If $a$ is the least upper bound of $s$ and $a \notin s$, then $a$ is a successor pre-limit element (i.e., there is no element $b$ such that $b \lessdot a$).
IsLUB.mem_of_not_isSuccPrelimit theorem
{s : Set α} (hs : IsLUB s a) (ha : ¬IsSuccPrelimit a) : a ∈ s
Full source 
lemma _root_.IsLUB.mem_of_not_isSuccPrelimit {s : Set α} (hs : IsLUB s a) (ha : ¬IsSuccPrelimit a) :
    a ∈ s :=
  ha.imp_symm hs.isSuccPrelimit_of_not_mem
Membership in Set for Non-Successor-Prelimit Least Upper Bounds
Informal description
Let $\alpha$ be a partially ordered set, $s \subseteq \alpha$ a subset, and $a \in \alpha$ an element. If $a$ is the least upper bound of $s$ and $a$ is not a successor pre-limit element (i.e., there exists some $b$ such that $b \lessdot a$), then $a$ belongs to $s$.
IsLUB.isSuccLimit_of_not_mem theorem
{s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) (ha : a ∉ s) : IsSuccLimit a
Full source 
lemma _root_.IsLUB.isSuccLimit_of_not_mem {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty)
    (ha : a ∉ s) : IsSuccLimit a := by
  refine ⟨?_, hs.isSuccPrelimit_of_not_mem ha⟩
  obtain ⟨b, hb⟩ := hs'
  obtain rfl | hb := (hs.1 hb).eq_or_lt
  · contradiction
  · exact hb.not_isMin
Least Upper Bound Outside Nonempty Set is Successor Limit
Informal description
Let $\alpha$ be a partially ordered set, $s \subseteq \alpha$ a nonempty subset, and $a \in \alpha$ an element. If $a$ is the least upper bound of $s$ and $a \notin s$, then $a$ is a successor limit element (i.e., $a$ is not minimal and there is no element $b$ such that $b \lessdot a$).
IsLUB.mem_of_not_isSuccLimit theorem
{s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) (ha : ¬IsSuccLimit a) : a ∈ s
Full source 
lemma _root_.IsLUB.mem_of_not_isSuccLimit {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty)
    (ha : ¬IsSuccLimit a) : a ∈ s :=
  ha.imp_symm <| hs.isSuccLimit_of_not_mem hs'
Membership in Set for Non-Successor-Limit Least Upper Bounds
Informal description
Let $\alpha$ be a partially ordered set, $s \subseteq \alpha$ a nonempty subset, and $a \in \alpha$ an element. If $a$ is the least upper bound of $s$ and $a$ is not a successor limit element (i.e., either $a$ is minimal or there exists some $b$ such that $b \lessdot a$), then $a$ belongs to $s$.
Order.IsSuccPrelimit.isLUB_Iio theorem
(ha : IsSuccPrelimit a) : IsLUB (Iio a) a
Full source 
theorem IsSuccPrelimit.isLUB_Iio (ha : IsSuccPrelimit a) : IsLUB (Iio a) a := by
  refine ⟨fun _ ↦ le_of_lt, fun b hb ↦ le_of_forall_lt fun c hc ↦ ?_⟩
  obtain ⟨d, hd, hd'⟩ := ha.lt_iff_exists_lt.1 hc
  exact hd'.trans_le (hb hd)
Successor Pre-Limit as Least Upper Bound of Strict Lower Set
Informal description
Let $a$ be a successor pre-limit element in a partially ordered set $\alpha$. Then $a$ is the least upper bound of the interval $(-\infty, a) = \{x \mid x < a\}$.
Order.IsSuccLimit.isLUB_Iio theorem
(ha : IsSuccLimit a) : IsLUB (Iio a) a
Full source 
theorem IsSuccLimit.isLUB_Iio (ha : IsSuccLimit a) : IsLUB (Iio a) a :=
  ha.isSuccPrelimit.isLUB_Iio
Successor Limit as Least Upper Bound of Strict Lower Set
Informal description
For any element $a$ in a partially ordered set that is a successor limit (i.e., $a$ is not minimal and does not cover any other element), $a$ is the least upper bound of the strict lower set $\{x \mid x < a\}$.
Order.isLUB_Iio_iff_isSuccPrelimit theorem
: IsLUB (Iio a) a ↔ IsSuccPrelimit a
Full source 
theorem isLUB_Iio_iff_isSuccPrelimit : IsLUBIsLUB (Iio a) a ↔ IsSuccPrelimit a := by
  refine ⟨fun ha b hb ↦ ?_, IsSuccPrelimit.isLUB_Iio⟩
  rw [hb.Iio_eq] at ha
  obtain rfl := isLUB_Iic.unique ha
  cases hb.lt.false
Characterization of Successor Pre-Limit via Least Upper Bound of Strict Lower Set
Informal description
For an element $a$ in a partially ordered set, $a$ is the least upper bound of the interval $(-\infty, a)$ if and only if $a$ is a successor pre-limit (i.e., there is no element $b$ such that $b \lessdot a$).
Order.IsSuccPrelimit.le_succ_iff theorem
(hb : IsSuccPrelimit b) : b ≤ succ a ↔ b ≤ a
Full source 
theorem IsSuccPrelimit.le_succ_iff (hb : IsSuccPrelimit b) : b ≤ succ a ↔ b ≤ a :=
  le_iff_le_iff_lt_iff_lt.2 hb.succ_lt_iff
Characterization of Successor Pre-Limit via Successor Inequality
Informal description
Let $b$ be a successor pre-limit element in a partially ordered set $\alpha$ equipped with a successor function $\text{succ}$. Then for any element $a \in \alpha$, the inequality $b \leq \text{succ}(a)$ holds if and only if $b \leq a$.
Order.IsSuccLimit.le_succ_iff theorem
(hb : IsSuccLimit b) : b ≤ succ a ↔ b ≤ a
Full source 
theorem IsSuccLimit.le_succ_iff (hb : IsSuccLimit b) : b ≤ succ a ↔ b ≤ a :=
  hb.isSuccPrelimit.le_succ_iff
Characterization of Successor Limit via Successor Inequality
Informal description
Let $b$ be a successor limit element in a partially ordered set $\alpha$ equipped with a successor function $\text{succ}$. Then for any element $a \in \alpha$, the inequality $b \leq \text{succ}(a)$ holds if and only if $b \leq a$.
Order.IsPredPrelimit definition
(a : α) : Prop
Full source 
/-- A predecessor pre-limit is a value that isn't covered by any other.

It's so named because in a predecessor order, a predecessor pre-limit can't be the predecessor of
anything smaller.

Use `IsPredLimit` to exclude the case of a maximal element. -/
def IsPredPrelimit (a : α) : Prop :=
  ∀ b, ¬ a ⋖ b
Predecessor pre-limit in an order
Informal description
An element $a$ in an ordered type $\alpha$ is called a *predecessor pre-limit* if it is not covered by any other element, i.e., there does not exist any $b$ such that $a$ is covered by $b$ (denoted $a \lessdot b$).
Order.not_isPredPrelimit_iff_exists_covBy theorem
(a : α) : ¬IsPredPrelimit a ↔ ∃ b, a ⋖ b
Full source 
theorem not_isPredPrelimit_iff_exists_covBy (a : α) : ¬IsPredPrelimit a¬IsPredPrelimit a ↔ ∃ b, a ⋖ b := by
  simp [IsPredPrelimit]
Characterization of Non-Predecessor-Prelimit Elements via Covering Relation
Informal description
An element $a$ in an ordered type $\alpha$ is not a predecessor pre-limit if and only if there exists some element $b$ such that $a$ is covered by $b$ (denoted $a \lessdot b$).
Order.IsPredPrelimit.of_dense theorem
[DenselyOrdered α] (a : α) : IsPredPrelimit a
Full source 
@[simp]
theorem IsPredPrelimit.of_dense [DenselyOrdered α] (a : α) : IsPredPrelimit a := fun _ => not_covBy
Dense Order Implies All Elements Are Predecessor Pre-Limits
Informal description
In a densely ordered type $\alpha$, every element $a$ is a predecessor pre-limit, meaning there does not exist any element $b$ such that $a$ is covered by $b$ (i.e., $a \lessdot b$).
Order.IsPredLimit definition
(a : α) : Prop
Full source 
/-- A predecessor limit is a value that isn't maximal and doesn't cover any other.

It's so named because in a predecessor order, a predecessor limit can't be the predecessor of
anything larger.

This previously allowed the element to be maximal. This usage is now covered by `IsPredPreLimit`. -/
def IsPredLimit (a : α) : Prop :=
  ¬ IsMax a¬ IsMax a ∧ IsPredPrelimit a
Predecessor limit in an order
Informal description
An element $a$ in an ordered type $\alpha$ is called a *predecessor limit* if it is not maximal and is a predecessor pre-limit, meaning there does not exist any $b$ such that $a$ is covered by $b$ (denoted $a \lessdot b$).
Order.IsPredLimit.not_isMax theorem
(h : IsPredLimit a) : ¬IsMax a
Full source 
protected theorem IsPredLimit.not_isMax (h : IsPredLimit a) : ¬ IsMax a := h.1
Predecessor limits are not maximal
Informal description
If an element $a$ in an ordered type $\alpha$ is a predecessor limit, then $a$ is not maximal.
Order.IsPredLimit.isPredPrelimit theorem
(h : IsPredLimit a) : IsPredPrelimit a
Full source 
protected theorem IsPredLimit.isPredPrelimit (h : IsPredLimit a) : IsPredPrelimit a := h.2
Predecessor limits are predecessor pre-limits
Informal description
If an element $a$ in an ordered type $\alpha$ is a predecessor limit, then it is also a predecessor pre-limit.
Order.isSuccLimit_toDual_iff theorem
: IsSuccLimit (toDual a) ↔ IsPredLimit a
Full source 
@[simp]
theorem isSuccLimit_toDual_iff : IsSuccLimitIsSuccLimit (toDual a) ↔ IsPredLimit a := by
  simp [IsSuccLimit, IsPredLimit]
Duality between successor and predecessor limits: $\mathrm{IsSuccLimit}(\mathrm{toDual}(a)) \leftrightarrow \mathrm{IsPredLimit}(a)$
Informal description
For any element $a$ in a partially ordered set $\alpha$, the dual element $\mathrm{toDual}(a)$ is a successor limit if and only if $a$ is a predecessor limit. Here, $\mathrm{toDual}(a)$ refers to the element $a$ in the order-dual of $\alpha$, and: - A *successor limit* is an element that is not minimal and does not cover any other element. - A *predecessor limit* is an element that is not maximal and is not covered by any other element.
Order.isPredLimit_toDual_iff theorem
: IsPredLimit (toDual a) ↔ IsSuccLimit a
Full source 
@[simp]
theorem isPredLimit_toDual_iff : IsPredLimitIsPredLimit (toDual a) ↔ IsSuccLimit a := by
  simp [IsSuccLimit, IsPredLimit]
Duality between predecessor and successor limits: $\mathrm{IsPredLimit}(\mathrm{toDual}(a)) \leftrightarrow \mathrm{IsSuccLimit}(a)$
Informal description
For any element $a$ in a partially ordered set $\alpha$, the dual element $\mathrm{toDual}(a)$ is a predecessor limit if and only if $a$ is a successor limit. Here: - A *predecessor limit* is an element that is not maximal and is not covered by any other element. - A *successor limit* is an element that is not minimal and does not cover any other element. - $\mathrm{toDual}(a)$ refers to the element $a$ in the order-dual of $\alpha$.
Order.IsPredPrelimit.isPredLimit_of_not_isMax theorem
(h : IsPredPrelimit a) (ha : ¬IsMax a) : IsPredLimit a
Full source 
theorem IsPredPrelimit.isPredLimit_of_not_isMax (h : IsPredPrelimit a) (ha : ¬ IsMax a) :
    IsPredLimit a :=
  ⟨ha, h⟩
Predecessor limit condition: from pre-limit and non-maximality
Informal description
For any element $a$ in an ordered type $\alpha$, if $a$ is a predecessor pre-limit and $a$ is not maximal, then $a$ is a predecessor limit.
Order.IsPredPrelimit.isPredLimit theorem
[NoMaxOrder α] (h : IsPredPrelimit a) : IsPredLimit a
Full source 
theorem IsPredPrelimit.isPredLimit [NoMaxOrder α] (h : IsPredPrelimit a) : IsPredLimit a :=
  h.isPredLimit_of_not_isMax (not_isMax a)
Predecessor limit condition in no-max orders: from pre-limit to limit
Informal description
In an order $\alpha$ with no maximal elements, if an element $a$ is a predecessor pre-limit (i.e., there is no $b$ such that $a \lessdot b$), then $a$ is a predecessor limit.
Order.isPredPrelimit_iff_isPredLimit_of_not_isMax theorem
(h : ¬IsMax a) : IsPredPrelimit a ↔ IsPredLimit a
Full source 
theorem isPredPrelimit_iff_isPredLimit_of_not_isMax (h : ¬ IsMax a) :
    IsPredPrelimitIsPredPrelimit a ↔ IsPredLimit a :=
  ⟨fun ha ↦ ha.isPredLimit_of_not_isMax h, IsPredLimit.isPredPrelimit⟩
Equivalence of Predecessor Pre-Limit and Predecessor Limit for Non-Maximal Elements
Informal description
For any element $a$ in an ordered type $\alpha$ that is not maximal, $a$ is a predecessor pre-limit if and only if $a$ is a predecessor limit.
Order.isPredPrelimit_iff_isPredLimit theorem
[NoMaxOrder α] : IsPredPrelimit a ↔ IsPredLimit a
Full source 
theorem isPredPrelimit_iff_isPredLimit [NoMaxOrder α] : IsPredPrelimitIsPredPrelimit a ↔ IsPredLimit a :=
  isPredPrelimit_iff_isPredLimit_of_not_isMax (not_isMax a)
Equivalence of Predecessor Pre-Limit and Predecessor Limit in No-Max Orders
Informal description
In an order $\alpha$ with no maximal elements, an element $a$ is a predecessor pre-limit if and only if it is a predecessor limit. That is, $a$ is not covered by any other element if and only if $a$ is not maximal and not covered by any other element.
IsMax.not_isPredLimit theorem
(h : IsMax a) : ¬IsPredLimit a
Full source 
protected theorem _root_.IsMax.not_isPredLimit (h : IsMax a) : ¬ IsPredLimit a :=
  fun ha ↦ ha.not_isMax h
Maximal Elements Are Not Predecessor Limits
Informal description
If an element $a$ in an ordered type $\alpha$ is maximal, then $a$ is not a predecessor limit.
IsMax.isPredPrelimit theorem
: IsMax a → IsPredPrelimit a
Full source 
protected theorem _root_.IsMax.isPredPrelimit : IsMax a → IsPredPrelimit a := fun h _ hab =>
  not_isMax_of_lt hab.lt h
Maximal Elements are Predecessor Pre-Limits
Informal description
If an element $a$ in an ordered type $\alpha$ is maximal (i.e., there is no element strictly greater than $a$), then $a$ is a predecessor pre-limit (i.e., there is no element that covers $a$).
Order.isPredPrelimit_top theorem
[OrderTop α] : IsPredPrelimit (⊤ : α)
Full source 
theorem isPredPrelimit_top [OrderTop α] : IsPredPrelimit (⊤ : α) :=
  isMax_top.isPredPrelimit
Greatest Element is a Predecessor Pre-Limit
Informal description
In an ordered type $\alpha$ with a greatest element $\top$, the element $\top$ is a predecessor pre-limit, meaning there is no element $b \in \alpha$ such that $\top$ is covered by $b$ (i.e., $\top \lessdot b$).
Order.IsPredLimit.ne_top theorem
[OrderTop α] (h : IsPredLimit a) : a ≠ ⊤
Full source 
theorem IsPredLimit.ne_top [OrderTop α] (h : IsPredLimit a) : a ≠ ⊤ :=
  h.dual.ne_bot
Predecessor Limit Elements are Not Top
Informal description
In an ordered type $\alpha$ with a greatest element $\top$, if an element $a$ is a predecessor limit, then $a$ is not equal to $\top$.
Order.not_isPredLimit_iff theorem
: ¬IsPredLimit a ↔ IsMax a ∨ ¬IsPredPrelimit a
Full source 
theorem not_isPredLimit_iff : ¬ IsPredLimit a¬ IsPredLimit a ↔ IsMax a ∨ ¬ IsPredPrelimit a := by
  rw [IsPredLimit, not_and_or, not_not]
Characterization of Non-Predecessor Limit Elements: $\neg\text{IsPredLimit}(a) \leftrightarrow \text{IsMax}(a) \lor \neg\text{IsPredPrelimit}(a)$
Informal description
An element $a$ in an ordered type $\alpha$ is not a predecessor limit if and only if it is either maximal or not a predecessor pre-limit.
Order.IsPredPrelimit.isMin theorem
(h : IsPredPrelimit (pred a)) : IsMin a
Full source 
protected theorem IsPredPrelimit.isMin (h : IsPredPrelimit (pred a)) : IsMin a :=
  h.dual.isMax
Minimality from Predecessor Pre-Limit Condition
Informal description
If the predecessor of an element $a$ in a preorder is a predecessor pre-limit, then $a$ is a minimal element.
Order.IsPredLimit.isMin theorem
(h : IsPredLimit (pred a)) : IsMin a
Full source 
protected theorem IsPredLimit.isMin (h : IsPredLimit (pred a)) : IsMin a :=
  h.dual.isMax
Minimality from Predecessor Limit Condition
Informal description
If the predecessor of an element $a$ in a preorder is a predecessor limit, then $a$ is a minimal element.
Order.not_isPredLimit_pred_of_not_isMin theorem
(ha : ¬IsMin a) : ¬IsPredLimit (pred a)
Full source 
theorem not_isPredLimit_pred_of_not_isMin (ha : ¬ IsMin a) : ¬ IsPredLimit (pred a) :=
  mt IsPredLimit.isMin ha
Non-minimal Elements Have Non-Limit Predecessors
Informal description
For any element $a$ in a preorder with a predecessor function, if $a$ is not minimal, then its predecessor $\mathrm{pred}(a)$ is not a predecessor limit.
Order.IsPredPrelimit.pred_ne theorem
(h : IsPredPrelimit a) (b : α) : pred b ≠ a
Full source 
theorem IsPredPrelimit.pred_ne (h : IsPredPrelimit a) (b : α) : predpred b ≠ a :=
  h.dual.succ_ne b
Predecessor of Any Element Differs from a Predecessor Pre-Limit
Informal description
For any element $a$ in a preorder $\alpha$, if $a$ is a predecessor pre-limit (i.e., there is no element covering $a$), then for any element $b \in \alpha$, the predecessor of $b$ is not equal to $a$.
Order.IsPredLimit.pred_ne theorem
(h : IsPredLimit a) (b : α) : pred b ≠ a
Full source 
theorem IsPredLimit.pred_ne (h : IsPredLimit a) (b : α) : predpred b ≠ a :=
  h.isPredPrelimit.pred_ne b
Predecessor Function Output Differs from Predecessor Limit Elements
Informal description
Let $\alpha$ be a preorder equipped with a predecessor function $\mathrm{pred}$. For any element $a \in \alpha$ that is a predecessor limit and for any element $b \in \alpha$, the predecessor of $b$ is not equal to $a$, i.e., $\mathrm{pred}(b) \neq a$.
Order.not_isPredPrelimit_pred theorem
(a : α) : ¬IsPredPrelimit (pred a)
Full source 
@[simp]
theorem not_isPredPrelimit_pred (a : α) : ¬ IsPredPrelimit (pred a) := fun h => h.pred_ne _ rfl
Predecessor of Any Element is Not a Predecessor Pre-Limit
Informal description
For any element $a$ in a preorder $\alpha$ equipped with a predecessor function, the predecessor of $a$ is not a predecessor pre-limit.
Order.not_isPredLimit_pred theorem
(a : α) : ¬IsPredLimit (pred a)
Full source 
@[simp]
theorem not_isPredLimit_pred (a : α) : ¬ IsPredLimit (pred a) := fun h => h.pred_ne _ rfl
Predecessor of Any Element is Not a Predecessor Limit
Informal description
For any element $a$ in a preorder $\alpha$ equipped with a predecessor function, the predecessor of $a$ is not a predecessor limit.
Order.IsPredPrelimit.isMax_of_noMin theorem
(h : IsPredPrelimit a) : IsMax a
Full source 
theorem IsPredPrelimit.isMax_of_noMin (h : IsPredPrelimit a) : IsMax a :=
  h.dual.isMin_of_noMax
Predecessor Pre-Limit Implies Maximal Element in Orders Without Minima
Informal description
If an element $a$ in a preorder $\alpha$ is a predecessor pre-limit (i.e., there is no element $b$ such that $a$ is covered by $b$) and $\alpha$ has no minimal elements, then $a$ is a maximal element of $\alpha$.
Order.not_isPredPrelimit_of_noMin theorem
[NoMaxOrder α] : ¬IsPredPrelimit a
Full source 
theorem not_isPredPrelimit_of_noMin [NoMaxOrder α] : ¬ IsPredPrelimit a := by simp
No predecessor pre-limits in orders without maxima
Informal description
In a preorder $\alpha$ with no maximal elements (i.e., a `NoMaxOrder`), no element $a \in \alpha$ is a predecessor pre-limit.
Order.isPredLimit_iff theorem
[OrderTop α] : IsPredLimit a ↔ a ≠ ⊤ ∧ IsPredPrelimit a
Full source 
theorem isPredLimit_iff [OrderTop α] : IsPredLimitIsPredLimit a ↔ a ≠ ⊤ ∧ IsPredPrelimit a := by
  rw [IsPredLimit, isMax_iff_eq_top]
Characterization of Predecessor Limits in Orders with Top Element
Informal description
Let $\alpha$ be an ordered type with a greatest element $\top$. An element $a \in \alpha$ is a predecessor limit if and only if $a \neq \top$ and $a$ is a predecessor pre-limit (i.e., there is no $b$ such that $a$ is covered by $b$).
Order.IsPredLimit.lt_top theorem
[OrderTop α] (h : IsPredLimit a) : a < ⊤
Full source 
theorem IsPredLimit.lt_top [OrderTop α] (h : IsPredLimit a) : a < ⊤ :=
  h.ne_top.lt_top
Predecessor Limit Elements are Strictly Below Top: $a < \top$
Informal description
Let $\alpha$ be an ordered type with a greatest element $\top$. If $a \in \alpha$ is a predecessor limit, then $a$ is strictly less than $\top$, i.e., $a < \top$.
Order.isPredPrelimit_of_pred_ne theorem
(h : ∀ b, pred b ≠ a) : IsPredPrelimit a
Full source 
theorem isPredPrelimit_of_pred_ne (h : ∀ b, predpred b ≠ a) : IsPredPrelimit a := fun b hba =>
  h b (CovBy.pred_eq hba)
Predecessor pre-limit criterion: $\forall b, \mathrm{pred}(b) \neq a$ implies $a$ is a predecessor pre-limit
Informal description
Let $\alpha$ be a preorder equipped with a predecessor function $\mathrm{pred} : \alpha \to \alpha$. If for every element $b \in \alpha$, $\mathrm{pred}(b) \neq a$, then $a$ is a predecessor pre-limit (i.e., there is no element covering $a$).
Order.not_isPredPrelimit_iff theorem
: ¬IsPredPrelimit a ↔ ∃ b, ¬IsMin b ∧ pred b = a
Full source 
theorem not_isPredPrelimit_iff : ¬ IsPredPrelimit a¬ IsPredPrelimit a ↔ ∃ b, ¬ IsMin b ∧ pred b = a := by
  rw [← isSuccPrelimit_toDual_iff]
  exact not_isSuccPrelimit_iff
Characterization of Non-Predecessor-Prelimit Elements via Non-Minimal Successors
Informal description
An element $a$ in a preorder $\alpha$ is *not* a predecessor pre-limit if and only if there exists an element $b$ that is not minimal and whose predecessor is $a$, i.e., $\mathrm{pred}(b) = a$.
Order.mem_range_pred_of_not_isPredPrelimit theorem
(h : ¬IsPredPrelimit a) : a ∈ range (pred : α → α)
Full source 
/-- See `not_isPredPrelimit_iff` for a version that states that `a` is a successor of a value other
than itself. -/
theorem mem_range_pred_of_not_isPredPrelimit (h : ¬ IsPredPrelimit a) :
    a ∈ range (pred : α → α) := by
  obtain ⟨b, hb⟩ := not_isPredPrelimit_iff.1 h
  exact ⟨b, hb.2⟩
Non-Predecessor-Prelimit Elements Belong to Predecessor Range
Informal description
If an element $a$ in a preorder $\alpha$ is not a predecessor pre-limit, then $a$ is in the range of the predecessor function, i.e., there exists some element $b \in \alpha$ such that $\mathrm{pred}(b) = a$.
Order.mem_range_pred_or_isPredPrelimit theorem
(a) : a ∈ range (pred : α → α) ∨ IsPredPrelimit a
Full source 
theorem mem_range_pred_or_isPredPrelimit (a) : a ∈ range (pred : α → α)a ∈ range (pred : α → α) ∨ IsPredPrelimit a :=
  or_iff_not_imp_right.2 <| mem_range_pred_of_not_isPredPrelimit
Decomposition of Elements into Predecessor Range or Predecessor Pre-Limit
Informal description
For any element $a$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, either $a$ is in the range of $\mathrm{pred}$ (i.e., there exists some $b \in \alpha$ such that $\mathrm{pred}(b) = a$) or $a$ is a predecessor pre-limit (i.e., there is no element covering $a$).
Order.isPredPrelimit_of_pred_lt theorem
(H : ∀ b > a, a < pred b) : IsPredPrelimit a
Full source 
theorem isPredPrelimit_of_pred_lt (H : ∀ b > a, a < pred b) : IsPredPrelimit a := fun a hab =>
  (H a hab.lt).ne (CovBy.pred_eq hab).symm
Characterization of Predecessor Pre-Limit via Predecessor Function
Informal description
Let $\alpha$ be a preorder equipped with a predecessor function $\mathrm{pred} : \alpha \to \alpha$. If for every element $b > a$ in $\alpha$, we have $a < \mathrm{pred}(b)$, then $a$ is a predecessor pre-limit element in $\alpha$.
Order.IsPredPrelimit.lt_pred theorem
(ha : IsPredPrelimit a) (hb : a < b) : a < pred b
Full source 
theorem IsPredPrelimit.lt_pred (ha : IsPredPrelimit a) (hb : a < b) : a < pred b :=
  ha.dual.succ_lt hb
Predecessor Pre-Limit Implies $a < \mathrm{pred}(b)$ for $a < b$
Informal description
Let $a$ be a predecessor pre-limit element in a preorder $\alpha$ (i.e., there is no element covering $a$), and let $b$ be an element such that $a < b$. Then $a$ is strictly less than the predecessor of $b$, i.e., $a < \mathrm{pred}(b)$.
Order.IsPredLimit.lt_pred theorem
(ha : IsPredLimit a) (hb : a < b) : a < pred b
Full source 
theorem IsPredLimit.lt_pred (ha : IsPredLimit a) (hb : a < b) : a < pred b :=
  ha.isPredPrelimit.lt_pred hb
Predecessor Limit Implies $a < \mathrm{pred}(b)$ for $a < b$
Informal description
Let $a$ be a predecessor limit element in a preorder $\alpha$ (i.e., $a$ is not maximal and there is no element covering $a$), and let $b$ be an element such that $a < b$. Then $a$ is strictly less than the predecessor of $b$, i.e., $a < \mathrm{pred}(b)$.
Order.IsPredPrelimit.lt_pred_iff theorem
(ha : IsPredPrelimit a) : a < pred b ↔ a < b
Full source 
theorem IsPredPrelimit.lt_pred_iff (ha : IsPredPrelimit a) : a < pred b ↔ a < b :=
  ha.dual.succ_lt_iff
Characterization of Predecessor Inequality for Pre-Limit Elements
Informal description
Let $a$ be a predecessor pre-limit element in a preorder $\alpha$ (i.e., there is no element covering $a$). Then for any element $b \in \alpha$, the inequality $a < \mathrm{pred}(b)$ holds if and only if $a < b$.
Order.IsPredLimit.lt_pred_iff theorem
(ha : IsPredLimit a) : a < pred b ↔ a < b
Full source 
theorem IsPredLimit.lt_pred_iff (ha : IsPredLimit a) : a < pred b ↔ a < b :=
  ha.dual.succ_lt_iff
Characterization of Predecessor Inequality for Predecessor Limit Elements
Informal description
For any predecessor limit element $a$ in a preorder $\alpha$ (i.e., $a$ is not maximal and there is no element covering $a$), the inequality $a < \mathrm{pred}(b)$ holds if and only if $a < b$ for any element $b \in \alpha$.
Order.isPredPrelimit_iff_lt_pred theorem
: IsPredPrelimit a ↔ ∀ b > a, a < pred b
Full source 
theorem isPredPrelimit_iff_lt_pred : IsPredPrelimitIsPredPrelimit a ↔ ∀ b > a, a < pred b :=
  ⟨fun hb _ => hb.lt_pred, isPredPrelimit_of_pred_lt⟩
Characterization of Predecessor Pre-Limit via Predecessor Function
Informal description
An element $a$ in a preorder $\alpha$ with a predecessor function $\mathrm{pred}$ is a predecessor pre-limit if and only if for every element $b > a$, we have $a < \mathrm{pred}(b)$.
Order.isPredPrelimit_iff_pred_ne theorem
: IsPredPrelimit a ↔ ∀ b, pred b ≠ a
Full source 
theorem isPredPrelimit_iff_pred_ne : IsPredPrelimitIsPredPrelimit a ↔ ∀ b, pred b ≠ a :=
  ⟨IsPredPrelimit.pred_ne, isPredPrelimit_of_pred_ne⟩
Characterization of predecessor pre-limits via predecessor inequality
Informal description
An element $a$ in a preorder $\alpha$ with a predecessor function is a predecessor pre-limit if and only if for every element $b \in \alpha$, the predecessor of $b$ is not equal to $a$. In other words, $a$ is a predecessor pre-limit precisely when it is not the predecessor of any element in $\alpha$.
Order.not_isPredPrelimit_iff' theorem
: ¬IsPredPrelimit a ↔ a ∈ range (pred : α → α)
Full source 
theorem not_isPredPrelimit_iff' : ¬ IsPredPrelimit a¬ IsPredPrelimit a ↔ a ∈ range (pred : α → α) := by
  simp_rw [isPredPrelimit_iff_pred_ne, not_forall, not_ne_iff, mem_range]
Characterization of Non-Predecessor-Prelimit Elements via Predecessor Function Range
Informal description
An element $a$ in a preorder $\alpha$ with a predecessor function is *not* a predecessor pre-limit if and only if $a$ is in the range of the predecessor function, i.e., there exists some $b \in \alpha$ such that $\mathrm{pred}(b) = a$.
Order.IsPredPrelimit.isMax theorem
(h : IsPredPrelimit a) : IsMax a
Full source 
protected theorem IsPredPrelimit.isMax (h : IsPredPrelimit a) : IsMax a :=
  h.dual.isMin
Predecessor Prelimit Implies Maximal Element
Informal description
If an element $a$ in a preorder $\alpha$ is a predecessor pre-limit (i.e., there is no element $b$ that covers $a$), then $a$ is a maximal element.
Order.not_isPredLimit theorem
: ¬IsPredLimit a
Full source 
@[simp]
theorem not_isPredLimit : ¬ IsPredLimit a :=
  fun h ↦ h.not_isMax <| h.isPredPrelimit.isMax
Non-predecessor-limit element in an order
Informal description
An element $a$ in an ordered type $\alpha$ is not a predecessor limit.
Order.not_isPredPrelimit theorem
[NoMaxOrder α] : ¬IsPredPrelimit a
Full source 
theorem not_isPredPrelimit [NoMaxOrder α] : ¬ IsPredPrelimit a := by simp
No predecessor pre-limits in orders without maxima
Informal description
In an order $\alpha$ with no maximal elements, no element $a \in \alpha$ is a predecessor pre-limit.
Order.IsPredPrelimit.le_iff_forall_le theorem
(h : IsPredPrelimit a) : b ≤ a ↔ ∀ ⦃c⦄, a < c → b ≤ c
Full source 
theorem IsPredPrelimit.le_iff_forall_le (h : IsPredPrelimit a) : b ≤ a ↔ ∀ ⦃c⦄, a < c → b ≤ c :=
  h.dual.le_iff_forall_le
Characterization of Order Relation for Predecessor Pre-Limit Elements
Informal description
Let $a$ be a predecessor pre-limit element in an ordered set $\alpha$. Then for any element $b \in \alpha$, we have $b \leq a$ if and only if for all $c > a$, it holds that $b \leq c$.
Order.IsPredLimit.le_iff_forall_le theorem
(h : IsPredLimit a) : b ≤ a ↔ ∀ ⦃c⦄, a < c → b ≤ c
Full source 
theorem IsPredLimit.le_iff_forall_le (h : IsPredLimit a) : b ≤ a ↔ ∀ ⦃c⦄, a < c → b ≤ c :=
  h.dual.le_iff_forall_le
Characterization of Order Relation for Predecessor Limit Elements
Informal description
Let $a$ be a predecessor limit element in an ordered set $\alpha$. Then for any element $b \in \alpha$, we have $b \leq a$ if and only if for all $c > a$, it holds that $b \leq c$.
Order.IsPredPrelimit.lt_iff_exists_lt theorem
(h : IsPredPrelimit b) : b < a ↔ ∃ c, b < c ∧ c < a
Full source 
theorem IsPredPrelimit.lt_iff_exists_lt (h : IsPredPrelimit b) : b < a ↔ ∃ c, b < c ∧ c < a :=
  h.dual.lt_iff_exists_lt
Characterization of Strict Order Relation for Predecessor Pre-Limit Elements
Informal description
Let $b$ be a predecessor pre-limit element in an ordered set $\alpha$. Then for any element $a \in \alpha$, we have $b < a$ if and only if there exists an element $c$ such that $b < c$ and $c < a$.
Order.IsPredLimit.lt_iff_exists_lt theorem
(h : IsPredLimit b) : b < a ↔ ∃ c, b < c ∧ c < a
Full source 
theorem IsPredLimit.lt_iff_exists_lt (h : IsPredLimit b) : b < a ↔ ∃ c, b < c ∧ c < a :=
  h.dual.lt_iff_exists_lt
Characterization of Strict Order Relation for Predecessor Limit Elements
Informal description
Let $b$ be a predecessor limit element in an ordered set $\alpha$. Then for any element $a \in \alpha$, the relation $b < a$ holds if and only if there exists an element $c$ such that $b < c$ and $c < a$.
IsGLB.isPredPrelimit_of_not_mem theorem
{s : Set α} (hs : IsGLB s a) (ha : a ∉ s) : IsPredPrelimit a
Full source 
lemma _root_.IsGLB.isPredPrelimit_of_not_mem {s : Set α} (hs : IsGLB s a) (ha : a ∉ s) :
    IsPredPrelimit a := by
  simpa using (IsGLB.dual hs).isSuccPrelimit_of_not_mem ha
Greatest lower bound outside set is predecessor pre-limit
Informal description
Let $\alpha$ be a partially ordered set, $s \subseteq \alpha$ a subset, and $a \in \alpha$ an element. If $a$ is the greatest lower bound of $s$ and $a \notin s$, then $a$ is a predecessor pre-limit element (i.e., there is no element $b$ such that $a \lessdot b$).
IsGLB.mem_of_not_isPredPrelimit theorem
{s : Set α} (hs : IsGLB s a) (ha : ¬IsPredPrelimit a) : a ∈ s
Full source 
lemma _root_.IsGLB.mem_of_not_isPredPrelimit {s : Set α} (hs : IsGLB s a) (ha : ¬IsPredPrelimit a) :
    a ∈ s :=
  ha.imp_symm hs.isPredPrelimit_of_not_mem
Membership in Set for Non-Predecessor-Prelimit Greatest Lower Bounds
Informal description
Let $\alpha$ be a partially ordered set, $s \subseteq \alpha$ a subset, and $a \in \alpha$ an element. If $a$ is the greatest lower bound of $s$ and $a$ is not a predecessor pre-limit (i.e., there exists some $b$ such that $a \lessdot b$), then $a$ must be an element of $s$.
IsGLB.isPredLimit_of_not_mem theorem
{s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty) (ha : a ∉ s) : IsPredLimit a
Full source 
lemma _root_.IsGLB.isPredLimit_of_not_mem {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty)
    (ha : a ∉ s) : IsPredLimit a := by
  simpa using (IsGLB.dual hs).isSuccLimit_of_not_mem hs' ha
Greatest Lower Bound Outside Nonempty Set is Predecessor Limit
Informal description
Let $\alpha$ be a partially ordered set, $s \subseteq \alpha$ a nonempty subset, and $a \in \alpha$ an element. If $a$ is the greatest lower bound of $s$ and $a \notin s$, then $a$ is a predecessor limit element (i.e., $a$ is not maximal and there is no element $b$ such that $a \lessdot b$).
IsGLB.mem_of_not_isPredLimit theorem
{s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty) (ha : ¬IsPredLimit a) : a ∈ s
Full source 
lemma _root_.IsGLB.mem_of_not_isPredLimit {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty)
    (ha : ¬IsPredLimit a) : a ∈ s :=
  ha.imp_symm <| hs.isPredLimit_of_not_mem hs'
Membership in Set for Non-Predecessor-Limit Greatest Lower Bounds
Informal description
Let $\alpha$ be a partially ordered set, $s \subseteq \alpha$ a nonempty subset, and $a \in \alpha$ an element. If $a$ is the greatest lower bound of $s$ and $a$ is not a predecessor limit (i.e., either $a$ is maximal or there exists some $b$ such that $a \lessdot b$), then $a$ must be an element of $s$.
Order.IsPredPrelimit.isGLB_Ioi theorem
(ha : IsPredPrelimit a) : IsGLB (Ioi a) a
Full source 
theorem IsPredPrelimit.isGLB_Ioi (ha : IsPredPrelimit a) : IsGLB (Ioi a) a :=
  ha.dual.isLUB_Iio
Predecessor Pre-Limit as Greatest Lower Bound of Strict Upper Interval
Informal description
Let $\alpha$ be a partially ordered set and $a \in \alpha$ a predecessor pre-limit element. Then $a$ is the greatest lower bound of the right-open interval $(a, \infty) = \{x \in \alpha \mid a < x\}$.
Order.IsPredLimit.isGLB_Ioi theorem
(ha : IsPredLimit a) : IsGLB (Ioi a) a
Full source 
theorem IsPredLimit.isGLB_Ioi (ha : IsPredLimit a) : IsGLB (Ioi a) a :=
  ha.dual.isLUB_Iio
Predecessor Limit as Greatest Lower Bound of Strict Upper Interval
Informal description
For any element $a$ in a partially ordered set that is a predecessor limit (i.e., $a$ is not maximal and does not cover any other element), $a$ is the greatest lower bound of the strict upper interval $\{x \mid a < x\}$.
Order.isGLB_Ioi_iff_isPredPrelimit theorem
: IsGLB (Ioi a) a ↔ IsPredPrelimit a
Full source 
theorem isGLB_Ioi_iff_isPredPrelimit : IsGLBIsGLB (Ioi a) a ↔ IsPredPrelimit a := by
  simpa using isLUB_Iio_iff_isSuccPrelimit (a := toDual a)
Characterization of Predecessor Pre-Limit via Greatest Lower Bound of Strict Upper Interval
Informal description
For an element $a$ in a partially ordered set, $a$ is the greatest lower bound of the interval $(a, \infty)$ if and only if $a$ is a predecessor pre-limit (i.e., there is no element $b$ such that $a \lessdot b$).
Order.IsPredPrelimit.pred_le_iff theorem
(hb : IsPredPrelimit b) : pred a ≤ b ↔ a ≤ b
Full source 
theorem IsPredPrelimit.pred_le_iff (hb : IsPredPrelimit b) : predpred a ≤ b ↔ a ≤ b :=
  hb.dual.le_succ_iff
Predecessor Inequality Characterization for Predecessor Pre-Limits
Informal description
For any element $b$ in a preorder $\alpha$ that is a predecessor pre-limit (i.e., $b$ is not covered by any other element), and for any element $a \in \alpha$, the inequality $\mathrm{pred}(a) \leq b$ holds if and only if $a \leq b$.
Order.IsPredLimit.pred_le_iff theorem
(hb : IsPredLimit b) : pred a ≤ b ↔ a ≤ b
Full source 
theorem IsPredLimit.pred_le_iff (hb : IsPredLimit b) : predpred a ≤ b ↔ a ≤ b :=
  hb.dual.le_succ_iff
Predecessor Inequality Characterization for Predecessor Limits
Informal description
For any element $b$ in a preorder $\alpha$ that is a predecessor limit (i.e., $b$ is not maximal and does not cover any other element), and for any element $a \in \alpha$, the inequality $\mathrm{pred}(a) \leq b$ holds if and only if $a \leq b$.
Order.isSuccPrelimitRecOn definition
: motive b
Full source 
/-- A value can be built by building it on successors and successor pre-limits. -/
@[elab_as_elim]
noncomputable def isSuccPrelimitRecOn : motive b :=
  if hb : IsSuccPrelimit b then isSuccPrelimit b hb else
    haveI H := Classical.choose_spec (not_isSuccPrelimit_iff.1 hb)
    cast (congr_arg motive H.2) (succ _ H.1)
Recursion on successor pre-limits
Informal description
Given a type $\alpha$ with a preorder and a successor function, the function `isSuccPrelimitRecOn` allows constructing an element of type `motive b` for any element $b$ in $\alpha$ by distinguishing two cases: if $b$ is a successor pre-limit (i.e., it does not cover any other element), then the construction uses a provided function `isSuccPrelimit`; otherwise, it uses the successor function `succ` on the element that $b$ covers.
Order.isSuccPrelimitRecOn_of_isSuccPrelimit theorem
(hb : IsSuccPrelimit b) : isSuccPrelimitRecOn b succ isSuccPrelimit = isSuccPrelimit b hb
Full source 
theorem isSuccPrelimitRecOn_of_isSuccPrelimit (hb : IsSuccPrelimit b) :
    isSuccPrelimitRecOn b succ isSuccPrelimit = isSuccPrelimit b hb :=
  dif_pos hb
Recursion on Successor Pre-Limit Elements
Informal description
For any element $b$ in a preorder $\alpha$ equipped with a successor function, if $b$ is a successor pre-limit (i.e., there is no element covered by $b$), then the recursion function `isSuccPrelimitRecOn` applied to $b$ with the successor function `succ` and the successor pre-limit case function `isSuccPrelimit` reduces to `isSuccPrelimit b hb`, where `hb` is the proof that $b$ is a successor pre-limit.
Order.isSuccPrelimitRecOn_succ_of_not_isMax theorem
(hb : ¬IsMax b) : isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb
Full source 
theorem isSuccPrelimitRecOn_succ_of_not_isMax (hb : ¬IsMax b) :
    isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb := by
  have hb' := not_isSuccPrelimit_succ_of_not_isMax hb
  have H := Classical.choose_spec (not_isSuccPrelimit_iff.1 hb')
  rw [isSuccPrelimitRecOn, dif_neg hb', cast_eq_iff_heq]
  congr
  exacts [(succ_eq_succ_iff_of_not_isMax H.1 hb).1 H.2, proof_irrel_heq _ _]
Recursion on Successor of Non-Maximal Elements in Preorders
Informal description
Let $\alpha$ be a preorder equipped with a successor function $\mathrm{succ}$. For any element $b \in \alpha$ that is not maximal, the recursion function $\mathrm{isSuccPrelimitRecOn}$ applied to $\mathrm{succ}(b)$ with the successor function $\mathrm{succ}$ and the successor pre-limit case function $\mathrm{isSuccPrelimit}$ reduces to $\mathrm{succ}(b, hb)$, where $hb$ is the proof that $b$ is not maximal.
Order.isSuccPrelimitRecOn_succ theorem
[NoMaxOrder α] (b : α) : isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b (not_isMax b)
Full source 
@[simp]
theorem isSuccPrelimitRecOn_succ [NoMaxOrder α] (b : α) :
    isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b (not_isMax b) :=
  isSuccPrelimitRecOn_succ_of_not_isMax _ _ _
Recursion on Successor in No-Max Preorder Yields Successor Function
Informal description
Let $\alpha$ be a preorder with no maximal elements, equipped with a successor function $\mathrm{succ}$. For any element $b \in \alpha$, the recursion function $\mathrm{isSuccPrelimitRecOn}$ applied to $\mathrm{succ}(b)$ with the successor function $\mathrm{succ}$ and the successor pre-limit case function $\mathrm{isSuccPrelimit}$ reduces to $\mathrm{succ}(b)$, where the proof that $b$ is not maximal is provided by $\mathrm{not\_isMax}$.
Order.isPredPrelimitRecOn definition
: motive b
Full source 
/-- A value can be built by building it on predecessors and predecessor pre-limits. -/
@[elab_as_elim]
noncomputable def isPredPrelimitRecOn : motive b :=
  isSuccPrelimitRecOn (α := αᵒᵈ) b pred (fun a ha ↦ isPredPrelimit a ha.dual)
Recursion on predecessor pre-limits
Informal description
Given a preorder $\alpha$ with a predecessor function, the function `isPredPrelimitRecOn` allows constructing an element of type `motive b` for any element $b$ in $\alpha$ by distinguishing two cases: if $b$ is a predecessor pre-limit (i.e., it does not cover any other element), then the construction uses a provided function `isPredPrelimit`; otherwise, it uses the predecessor function `pred` on the element that $b$ covers.
Order.isPredPrelimitRecOn_of_isPredPrelimit theorem
(hb : IsPredPrelimit b) : isPredPrelimitRecOn b pred isPredPrelimit = isPredPrelimit b hb
Full source 
theorem isPredPrelimitRecOn_of_isPredPrelimit (hb : IsPredPrelimit b) :
    isPredPrelimitRecOn b pred isPredPrelimit = isPredPrelimit b hb :=
  isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.dual
Recursion on Predecessor Pre-Limit Elements Yields Pre-Limit Case
Informal description
For any element $b$ in a preorder $\alpha$ equipped with a predecessor function, if $b$ is a predecessor pre-limit (i.e., there is no element covered by $b$), then the recursion function `isPredPrelimitRecOn` applied to $b$ with the predecessor function `pred` and the predecessor pre-limit case function `isPredPrelimit` reduces to `isPredPrelimit b hb$, where `hb` is the proof that $b$ is a predecessor pre-limit.
Order.isPredPrelimitRecOn_pred_of_not_isMin theorem
(hb : ¬IsMin b) : isPredPrelimitRecOn (Order.pred b) pred isPredPrelimit = pred b hb
Full source 
theorem isPredPrelimitRecOn_pred_of_not_isMin (hb : ¬IsMin b) :
    isPredPrelimitRecOn (Order.pred b) pred isPredPrelimit = pred b hb :=
  isSuccPrelimitRecOn_succ_of_not_isMax (α := αᵒᵈ) _ _ _
Recursion on Predecessor of Non-Minimal Elements Yields Predecessor Function
Informal description
For any element $b$ in a preorder $\alpha$ equipped with a predecessor function, if $b$ is not minimal, then the recursion function `isPredPrelimitRecOn` applied to the predecessor of $b$ with the predecessor function `pred` and the predecessor pre-limit case function `isPredPrelimit` reduces to `pred b hb`, where `hb` is the proof that $b$ is not minimal.
Order.isPredPrelimitRecOn_pred theorem
[NoMinOrder α] (b : α) : isPredPrelimitRecOn (Order.pred b) pred isPredPrelimit = pred b (not_isMin b)
Full source 
@[simp]
theorem isPredPrelimitRecOn_pred [NoMinOrder α] (b : α) :
    isPredPrelimitRecOn (Order.pred b) pred isPredPrelimit = pred b (not_isMin b) :=
  isPredPrelimitRecOn_pred_of_not_isMin _ _ _
Recursion on Predecessor in No-Min-Order Yields Predecessor Function
Informal description
In a preorder $\alpha$ with no minimal elements (i.e., a `NoMinOrder`), for any element $b \in \alpha$, the recursion function `isPredPrelimitRecOn` applied to the predecessor of $b$ (denoted $\mathrm{pred}(b)$) with the predecessor function `pred` and the predecessor pre-limit case function `isPredPrelimit` reduces to the predecessor function evaluated at $b$ with the proof that $b$ is not minimal.
Order.isSuccLimitRecOn definition
: motive b
Full source 
/-- A value can be built by building it on minimal elements, successors, and successor limits. -/
@[elab_as_elim]
noncomputable def isSuccLimitRecOn : motive b :=
  isSuccPrelimitRecOn b succ fun a ha ↦
    if h : IsMin a then isMin a h else isSuccLimit a (ha.isSuccLimit_of_not_isMin h)
Recursion on successor limits, minimal elements, and successors
Informal description
Given a type $\alpha$ with a preorder and a successor function, the function `isSuccLimitRecOn` allows constructing an element of type `motive b` for any element $b$ in $\alpha$ by distinguishing three cases: 1. If $b$ is a minimal element, the construction uses a provided function `isMin`. 2. If $b$ is the successor of some element $a$, the construction uses the successor function `succ` on $a$. 3. If $b$ is a successor limit (i.e., not minimal and does not cover any element), the construction uses a provided function `isSuccLimit`. This is a generalization of recursion on successor limits, minimal elements, and successors.
Order.isSuccLimitRecOn_of_isSuccLimit theorem
(hb : IsSuccLimit b) : isSuccLimitRecOn b isMin succ isSuccLimit = isSuccLimit b hb
Full source 
@[simp]
theorem isSuccLimitRecOn_of_isSuccLimit (hb : IsSuccLimit b) :
    isSuccLimitRecOn b isMin succ isSuccLimit = isSuccLimit b hb := by
  rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit,
    dif_neg hb.not_isMin]
Recursion on successor limits reduces to successor limit case
Informal description
For any element $b$ in a preorder $\alpha$ equipped with a successor function, if $b$ is a successor limit (i.e., not minimal and does not cover any element), then the recursion function `isSuccLimitRecOn` applied to $b$ with the minimal case function `isMin`, the successor function `succ`, and the successor limit case function `isSuccLimit` reduces to `isSuccLimit b hb$, where `hb` is the proof that $b$ is a successor limit.
Order.isSuccLimitRecOn_succ_of_not_isMax theorem
(hb : ¬IsMax b) : isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb
Full source 
theorem isSuccLimitRecOn_succ_of_not_isMax (hb : ¬IsMax b) :
    isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb := by
  rw [isSuccLimitRecOn, isSuccPrelimitRecOn_succ_of_not_isMax]
Recursion on successor of non-maximal elements reduces to successor case
Informal description
Let $\alpha$ be a preorder equipped with a successor function $\mathrm{succ}$. For any element $b \in \alpha$ that is not maximal, the recursion function $\mathrm{isSuccLimitRecOn}$ applied to $\mathrm{succ}(b)$ with the minimal case function $\mathrm{isMin}$, the successor function $\mathrm{succ}$, and the successor limit case function $\mathrm{isSuccLimit}$ reduces to $\mathrm{succ}(b, hb)$, where $hb$ is the proof that $b$ is not maximal.
Order.isSuccLimitRecOn_succ theorem
[NoMaxOrder α] (b : α) : isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b (not_isMax b)
Full source 
@[simp]
theorem isSuccLimitRecOn_succ [NoMaxOrder α] (b : α) :
    isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b (not_isMax b) :=
  isSuccLimitRecOn_succ_of_not_isMax isMin succ isSuccLimit _
Recursion on successors in a NoMaxOrder reduces to successor case
Informal description
Let $\alpha$ be a preorder with no maximal elements, equipped with a successor function $\mathrm{succ}$. For any element $b \in \alpha$, the recursion function $\mathrm{isSuccLimitRecOn}$ applied to $\mathrm{succ}(b)$ with the minimal case function $\mathrm{isMin}$, the successor function $\mathrm{succ}$, and the successor limit case function $\mathrm{isSuccLimit}$ reduces to $\mathrm{succ}(b)$, where the proof that $b$ is not maximal is given by $\mathrm{not\_isMax}\ b$.
Order.isSuccLimitRecOn_of_isMin theorem
(hb : IsMin b) : isSuccLimitRecOn b isMin succ isSuccLimit = isMin b hb
Full source 
theorem isSuccLimitRecOn_of_isMin (hb : IsMin b) :
    isSuccLimitRecOn b isMin succ isSuccLimit = isMin b hb := by
  rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]
Recursion on Minimal Elements in Successor Limit Context
Informal description
For any element $b$ in a preorder $\alpha$ equipped with a successor function, if $b$ is a minimal element (i.e., there is no element strictly less than $b$), then the recursion function `isSuccLimitRecOn` applied to $b$ with the minimal case function `isMin`, successor function `succ`, and successor limit case function `isSuccLimit` reduces to `isMin b hb`, where `hb` is the proof that $b$ is minimal.
Order.isPredLimitRecOn definition
: motive b
Full source 
/-- A value can be built by building it on maximal elements, predecessors,
and predecessor limits. -/
@[elab_as_elim]
noncomputable def isPredLimitRecOn : motive b :=
  isSuccLimitRecOn (α := αᵒᵈ) b isMax pred (fun a ha => isPredLimit a ha.dual)
Recursion on predecessor limits, maximal elements, and predecessors
Informal description
Given a type $\alpha$ with a preorder and a predecessor function, the function `isPredLimitRecOn` allows constructing an element of type `motive b` for any element $b$ in $\alpha$ by distinguishing three cases: 1. If $b$ is a maximal element, the construction uses a provided function `isMax`. 2. If $b$ is the predecessor of some element $a$, the construction uses the predecessor function `pred` on $a$. 3. If $b$ is a predecessor limit (i.e., not maximal and does not cover any element), the construction uses a provided function `isPredLimit`. This is a generalization of recursion on predecessor limits, maximal elements, and predecessors.
Order.isPredLimitRecOn_of_isPredLimit theorem
(hb : IsPredLimit b) : isPredLimitRecOn b isMax pred isPredLimit = isPredLimit b hb
Full source 
@[simp]
theorem isPredLimitRecOn_of_isPredLimit (hb : IsPredLimit b) :
    isPredLimitRecOn b isMax pred isPredLimit = isPredLimit b hb :=
  isSuccLimitRecOn_of_isSuccLimit (α := αᵒᵈ) isMax pred _ hb.dual
Recursion on Predecessor Limits Reduces to Predecessor Limit Case
Informal description
For any element $b$ in a preorder $\alpha$ with a predecessor function, if $b$ is a predecessor limit (i.e., not maximal and does not cover any element), then the recursion function `isPredLimitRecOn` applied to $b$ with the maximal case function `isMax`, predecessor function `pred`, and predecessor limit case function `isPredLimit` reduces to `isPredLimit b hb`, where `hb` is the proof that $b$ is a predecessor limit.
Order.isPredLimitRecOn_pred_of_not_isMin theorem
(hb : ¬IsMin b) : isPredLimitRecOn (Order.pred b) isMax pred isPredLimit = pred b hb
Full source 
theorem isPredLimitRecOn_pred_of_not_isMin (hb : ¬IsMin b) :
    isPredLimitRecOn (Order.pred b) isMax pred isPredLimit = pred b hb :=
  isSuccLimitRecOn_succ_of_not_isMax (α := αᵒᵈ) isMax pred _ hb
Recursion on Predecessor of Non-Minimal Elements Reduces to Predecessor Case
Informal description
For any element $b$ in a preorder $\alpha$ equipped with a predecessor function, if $b$ is not minimal, then the recursion function `isPredLimitRecOn` applied to the predecessor of $b$ with the maximal case function `isMax`, predecessor function `pred`, and predecessor limit case function `isPredLimit` reduces to `pred b hb`, where `hb` is the proof that $b$ is not minimal.
Order.isPredLimitRecOn_pred theorem
[NoMinOrder α] : isPredLimitRecOn (Order.pred b) isMax pred isPredLimit = pred b (not_isMin b)
Full source 
@[simp]
theorem isPredLimitRecOn_pred [NoMinOrder α] :
    isPredLimitRecOn (Order.pred b) isMax pred isPredLimit = pred b (not_isMin b) :=
  isSuccLimitRecOn_succ (α := αᵒᵈ) isMax pred _ b
Recursion on Predecessor in NoMinOrder Reduces to Predecessor Case
Informal description
Let $\alpha$ be a preorder with no minimal elements, equipped with a predecessor function $\mathrm{pred}$. For any element $b \in \alpha$, the recursion function $\mathrm{isPredLimitRecOn}$ applied to $\mathrm{pred}(b)$ with the maximal case function $\mathrm{isMax}$, predecessor function $\mathrm{pred}$, and predecessor limit case function $\mathrm{isPredLimit}$ reduces to $\mathrm{pred}(b)$, where the proof that $b$ is not minimal is given by $\mathrm{not\_isMin}\ b$.
Order.isPredLimitRecOn_of_isMax theorem
(hb : IsMax b) : isPredLimitRecOn b isMax pred isPredLimit = isMax b hb
Full source 
theorem isPredLimitRecOn_of_isMax (hb : IsMax b) :
    isPredLimitRecOn b isMax pred isPredLimit = isMax b hb :=
  isSuccLimitRecOn_of_isMin (α := αᵒᵈ) isMax pred _ hb
Recursion on Maximal Elements in Predecessor Limit Context
Informal description
For any element $b$ in a preorder $\alpha$ equipped with a predecessor function, if $b$ is a maximal element (i.e., there is no element strictly greater than $b$), then the recursion function `isPredLimitRecOn` applied to $b$ with the maximal case function `isMax`, predecessor function `pred`, and predecessor limit case function `isPredLimit` reduces to `isMax b hb`, where `hb` is the proof that $b$ is maximal.
SuccOrder.prelimitRecOn definition
: motive b
Full source 
/-- Recursion principle on a well-founded partial `SuccOrder`. -/
@[elab_as_elim] noncomputable def prelimitRecOn : motive b :=
  wellFounded_lt.fix
    (fun a IH ↦ if h : IsSuccPrelimit a then isSuccPrelimit a h IH else
      haveI H := Classical.choose_spec (not_isSuccPrelimit_iff.1 h)
      cast (congr_arg motive H.2) (succ _ H.1 <| IH _ <| H.2.subst <| lt_succ_of_not_isMax H.1))
    b
Recursion principle on a well-founded successor order
Informal description
The recursion principle on a well-founded partial order with a successor function. Given a motive `motive`, a successor function `succ`, and a predicate `isSuccPrelimit`, this defines a recursive function that evaluates to `isSuccPrelimit b h IH` if `b` is a successor pre-limit (where `IH` is the recursive call on elements less than `b`), and otherwise evaluates to `succ b h (prelimitRecOn b succ isSuccPrelimit)` where `h` is a proof that `b` is not maximal.
SuccOrder.prelimitRecOn_of_isSuccPrelimit theorem
(hb : IsSuccPrelimit b) : prelimitRecOn b succ isSuccPrelimit = isSuccPrelimit b hb fun x _ ↦ SuccOrder.prelimitRecOn x succ isSuccPrelimit
Full source 
@[simp]
theorem prelimitRecOn_of_isSuccPrelimit (hb : IsSuccPrelimit b) :
    prelimitRecOn b succ isSuccPrelimit =
      isSuccPrelimit b hb fun x _ ↦ SuccOrder.prelimitRecOn x succ isSuccPrelimit := by
  rw [prelimitRecOn, WellFounded.fix_eq, dif_pos hb]; rfl
Recursion on Successor Pre-Limit Elements
Informal description
For any element $b$ in a partially ordered set $\alpha$ with a successor function, if $b$ is a successor pre-limit (i.e., there is no element covered by $b$), then the recursive function `prelimitRecOn` evaluated at $b$ equals the application of the successor pre-limit predicate to $b$ and the recursive function evaluated at all elements less than $b$.
SuccOrder.prelimitRecOn_succ_of_not_isMax theorem
(hb : ¬IsMax b) : prelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb (prelimitRecOn b succ isSuccPrelimit)
Full source 
theorem prelimitRecOn_succ_of_not_isMax (hb : ¬IsMax b) :
    prelimitRecOn (Order.succ b) succ isSuccPrelimit =
      succ b hb (prelimitRecOn b succ isSuccPrelimit) := by
  have h := not_isSuccPrelimit_succ_of_not_isMax hb
  have H := Classical.choose_spec (not_isSuccPrelimit_iff.1 h)
  rw [prelimitRecOn, WellFounded.fix_eq, dif_neg h]
  have {a c : α} {ha hc} {x : ∀ a, motive a} (h : a = c) :
    cast (congr_arg (motive ∘ Order.succ) h) (succ a ha (x a)) = succ c hc (x c) := by subst h; rfl
  exact this <| (succ_eq_succ_iff_of_not_isMax H.1 hb).1 H.2
Recursion on Successor of Non-Maximal Elements in a Partial Order
Informal description
For any element $b$ in a partially ordered set $\alpha$ with a successor function, if $b$ is not maximal, then the recursive function `prelimitRecOn` evaluated at the successor of $b$ equals the application of the successor function to $b$ and the recursive function evaluated at $b$. In symbols: $$ \text{prelimitRecOn}(\text{succ}(b)) = \text{succ}(b, h_b, \text{prelimitRecOn}(b)) $$ where $h_b$ is a proof that $b$ is not maximal.
SuccOrder.prelimitRecOn_succ theorem
[NoMaxOrder α] (b : α) : prelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b (not_isMax b) (prelimitRecOn b succ isSuccPrelimit)
Full source 
@[simp]
theorem prelimitRecOn_succ [NoMaxOrder α] (b : α) :
    prelimitRecOn (Order.succ b) succ isSuccPrelimit =
      succ b (not_isMax b) (prelimitRecOn b succ isSuccPrelimit) :=
  prelimitRecOn_succ_of_not_isMax _ _ _
Recursion on Successor in a No-Max-Order
Informal description
Let $\alpha$ be a partial order with no maximal elements. For any element $b \in \alpha$, the recursive function `prelimitRecOn` evaluated at the successor of $b$ equals the application of the successor function to $b$, where the proof that $b$ is not maximal is given by `not_isMax b`, and the recursive function evaluated at $b$. In symbols: $$ \text{prelimitRecOn}(\text{succ}(b)) = \text{succ}(b, \text{not\_isMax}(b), \text{prelimitRecOn}(b)) $$
SuccOrder.limitRecOn definition
: motive b
Full source 
/-- Recursion principle on a well-founded partial `SuccOrder`, separating out the case of a
minimal element. -/
@[elab_as_elim] noncomputable def limitRecOn : motive b :=
  prelimitRecOn b succ fun a ha IH ↦
    if h : IsMin a then isMin a h else isSuccLimit a (ha.isSuccLimit_of_not_isMin h) IH
Recursion principle for successor limits in a well-founded order
Informal description
The recursion principle on a well-founded partial order with a successor function, separating out the case of a minimal element. Given a motive `motive`, a successor function `succ`, and a predicate `isSuccLimit`, this defines a recursive function that evaluates to `isMin b h` if `b` is a minimal element (where `h` is a proof of minimality), and otherwise evaluates to `isSuccLimit b h IH` where `h` is a proof that `b` is a successor limit and `IH` is the recursive call on elements less than `b`.
SuccOrder.limitRecOn_isMin theorem
(hb : IsMin b) : limitRecOn b isMin succ isSuccLimit = isMin b hb
Full source 
@[simp]
theorem limitRecOn_isMin (hb : IsMin b) : limitRecOn b isMin succ isSuccLimit = isMin b hb := by
  rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]
Recursion on Minimal Elements in Successor Order
Informal description
For any minimal element $b$ in a well-founded partial order with a successor function, the recursive function `limitRecOn` evaluated at $b$ equals the application of the minimality predicate to $b$ with the proof of minimality $hb$.
SuccOrder.limitRecOn_of_isSuccLimit theorem
(hb : IsSuccLimit b) : limitRecOn b isMin succ isSuccLimit = isSuccLimit b hb fun x _ ↦ limitRecOn x isMin succ isSuccLimit
Full source 
@[simp]
theorem limitRecOn_of_isSuccLimit (hb : IsSuccLimit b) :
    limitRecOn b isMin succ isSuccLimit =
      isSuccLimit b hb fun x _ ↦ limitRecOn x isMin succ isSuccLimit := by
  rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_neg hb.not_isMin]; rfl
Recursion on Successor Limit Elements
Informal description
Let $\alpha$ be a well-founded partial order with a successor function, and let $b \in \alpha$ be a successor limit element (i.e., $b$ is not minimal and does not cover any other element). Then the recursive function `limitRecOn` evaluated at $b$ equals the application of the successor limit predicate to $b$ and the recursive function evaluated at all elements less than $b$.
SuccOrder.limitRecOn_succ_of_not_isMax theorem
(hb : ¬IsMax b) : limitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb (limitRecOn b isMin succ isSuccLimit)
Full source 
theorem limitRecOn_succ_of_not_isMax (hb : ¬IsMax b) :
    limitRecOn (Order.succ b) isMin succ isSuccLimit =
      succ b hb (limitRecOn b isMin succ isSuccLimit) := by
  rw [limitRecOn, prelimitRecOn_succ_of_not_isMax]; rfl
Recursion on Successor of Non-Maximal Elements in a Well-Founded Order
Informal description
Let $\alpha$ be a well-founded partial order with a successor function $\text{succ}$, and let $b \in \alpha$ be a non-maximal element. Then the recursive function $\text{limitRecOn}$ evaluated at $\text{succ}(b)$ equals the successor of $b$ applied to the recursive function evaluated at $b$. In symbols: $$\text{limitRecOn}(\text{succ}(b)) = \text{succ}(b, h_b, \text{limitRecOn}(b))$$ where $h_b$ is a proof that $b$ is not maximal.
SuccOrder.limitRecOn_succ theorem
[NoMaxOrder α] (b : α) : limitRecOn (Order.succ b) isMin succ isSuccLimit = succ b (not_isMax b) (limitRecOn b isMin succ isSuccLimit)
Full source 
@[simp]
theorem limitRecOn_succ [NoMaxOrder α] (b : α) :
    limitRecOn (Order.succ b) isMin succ isSuccLimit =
      succ b (not_isMax b) (limitRecOn b isMin succ isSuccLimit) :=
  limitRecOn_succ_of_not_isMax isMin succ isSuccLimit _
Recursion on Successor in a No-Max-Order
Informal description
Let $\alpha$ be a partial order with no maximal elements (i.e., a `NoMaxOrder`). For any element $b \in \alpha$, the recursive function `limitRecOn` evaluated at the successor of $b$ equals the successor function applied to $b$ (with proof that $b$ is not maximal) and the recursive function evaluated at $b$. In symbols: $$\text{limitRecOn}(\text{succ}(b)) = \text{succ}(b, \text{not\_isMax}(b), \text{limitRecOn}(b))$$
PredOrder.prelimitRecOn definition
: motive b
Full source 
/-- Recursion principle on a well-founded partial `PredOrder`. -/
@[elab_as_elim] noncomputable def prelimitRecOn : motive b :=
  SuccOrder.prelimitRecOn (α := αᵒᵈ) b pred (fun a ha => isPredPrelimit a ha.dual)
Recursion principle for predecessor pre-limits in a well-founded order
Informal description
The recursion principle for a well-founded partial order with a predecessor function. Given a predicate `isPredPrelimit` and a predecessor function `pred`, this defines a recursive function that evaluates to `isPredPrelimit b h IH` if `b` is a predecessor pre-limit (where `IH` is the recursive call on elements greater than `b`), and otherwise evaluates to `pred b h (prelimitRecOn b pred isPredPrelimit)` where `h` is a proof that `b` is not minimal.
PredOrder.prelimitRecOn_of_isPredPrelimit theorem
(hb : IsPredPrelimit b) : prelimitRecOn b pred isPredPrelimit = isPredPrelimit b hb fun x _ ↦ prelimitRecOn x pred isPredPrelimit
Full source 
@[simp]
theorem prelimitRecOn_of_isPredPrelimit (hb : IsPredPrelimit b) :
    prelimitRecOn b pred isPredPrelimit =
      isPredPrelimit b hb fun x _ ↦ prelimitRecOn x pred isPredPrelimit :=
  SuccOrder.prelimitRecOn_of_isSuccPrelimit _ _ hb.dual
Recursion on Predecessor Pre-Limit Elements
Informal description
For any element $b$ in a partially ordered set $\alpha$ with a predecessor function, if $b$ is a predecessor pre-limit (i.e., there is no element covering $b$), then the recursive function `prelimitRecOn` evaluated at $b$ equals the application of the predecessor pre-limit predicate to $b$ and the recursive function evaluated at all elements less than $b$.
PredOrder.prelimitRecOn_pred_of_not_isMin theorem
(hb : ¬IsMin b) : prelimitRecOn (Order.pred b) pred isPredPrelimit = pred b hb (prelimitRecOn b pred isPredPrelimit)
Full source 
theorem prelimitRecOn_pred_of_not_isMin (hb : ¬IsMin b) :
    prelimitRecOn (Order.pred b) pred isPredPrelimit =
      pred b hb (prelimitRecOn b pred isPredPrelimit) :=
  SuccOrder.prelimitRecOn_succ_of_not_isMax _ _ _
Recursion on Predecessor of Non-Minimal Elements
Informal description
For any element $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, if $b$ is not minimal, then the recursive function $\mathrm{prelimitRecOn}$ evaluated at $\mathrm{pred}(b)$ equals the application of $\mathrm{pred}$ to $b$ and the recursive function evaluated at $b$. In symbols: $$ \mathrm{prelimitRecOn}(\mathrm{pred}(b)) = \mathrm{pred}(b, h_b, \mathrm{prelimitRecOn}(b)) $$ where $h_b$ is a proof that $b$ is not minimal.
PredOrder.prelimitRecOn_pred theorem
[NoMinOrder α] (b : α) : prelimitRecOn (Order.pred b) pred isPredPrelimit = pred b (not_isMin b) (prelimitRecOn b pred isPredPrelimit)
Full source 
@[simp]
theorem prelimitRecOn_pred [NoMinOrder α] (b : α) :
    prelimitRecOn (Order.pred b) pred isPredPrelimit =
      pred b (not_isMin b) (prelimitRecOn b pred isPredPrelimit) :=
  prelimitRecOn_pred_of_not_isMin _ _ _
Recursion on Predecessor in No-Minimal-Elements Order
Informal description
Let $\alpha$ be a preorder with no minimal elements, equipped with a predecessor function $\mathrm{pred} : \alpha \to \alpha$ and a predicate $\mathrm{isPredPrelimit}$ identifying predecessor pre-limits. For any element $b \in \alpha$, the recursive function $\mathrm{prelimitRecOn}$ evaluated at $\mathrm{pred}(b)$ equals the application of $\mathrm{pred}$ to $b$ and the recursive function evaluated at $b$. That is: $$ \mathrm{prelimitRecOn}(\mathrm{pred}(b)) = \mathrm{pred}(b, \text{not\_isMin } b, \mathrm{prelimitRecOn}(b)) $$ where $\text{not\_isMin } b$ is a proof that $b$ is not minimal (which exists since $\alpha$ has no minimal elements).
PredOrder.limitRecOn definition
: motive b
Full source 
/-- Recursion principle on a well-founded partial `PredOrder`, separating out the case of a
maximal element. -/
@[elab_as_elim] noncomputable def limitRecOn : motive b :=
  SuccOrder.limitRecOn (α := αᵒᵈ) b isMax pred (fun a ha => isPredLimit a ha.dual)
Recursion principle for predecessor limits in well-founded orders
Informal description
Recursion principle for predecessor limits in a well-founded partial order with a predecessor function, separating out the case of a maximal element. Given: - A motive `motive : α → Sort*` - A proof `isMax` that handles maximal elements - A predecessor function `pred` that handles non-maximal elements - A predicate `isPredLimit` identifying predecessor limits The principle defines a recursive function that: 1. For a maximal element `b`, evaluates to `isMax b h` (where `h` proves maximality) 2. Otherwise, evaluates to `isPredLimit b h IH` where `h` proves `b` is a predecessor limit and `IH` is the recursive call on elements greater than `b` This is defined via duality from the successor limit recursion principle applied to the order dual.
PredOrder.limitRecOn_isMax theorem
(hb : IsMax b) : limitRecOn b isMax pred isPredLimit = isMax b hb
Full source 
@[simp]
theorem limitRecOn_isMax (hb : IsMax b) : limitRecOn b isMax pred isPredLimit = isMax b hb :=
  SuccOrder.limitRecOn_isMin (α := αᵒᵈ) isMax pred _ hb
Recursion on Maximal Elements in Predecessor Order
Informal description
For any maximal element $b$ in a well-founded partial order with a predecessor function, the recursive function `limitRecOn` evaluated at $b$ equals the application of the maximality predicate to $b$ with the proof of maximality $hb$.
PredOrder.limitRecOn_of_isPredLimit theorem
(hb : IsPredLimit b) : limitRecOn b isMax pred isPredLimit = isPredLimit b hb fun x _ ↦ limitRecOn x isMax pred isPredLimit
Full source 
@[simp]
theorem limitRecOn_of_isPredLimit (hb : IsPredLimit b) :
    limitRecOn b isMax pred isPredLimit =
      isPredLimit b hb fun x _ ↦ limitRecOn x isMax pred isPredLimit :=
  SuccOrder.limitRecOn_of_isSuccLimit (α := αᵒᵈ) isMax pred _ hb.dual
Recursion on Predecessor Limit Elements
Informal description
Let $\alpha$ be a well-founded partial order with a predecessor function, and let $b \in \alpha$ be a predecessor limit element (i.e., $b$ is not maximal and does not cover any other element). Then the recursive function `limitRecOn` evaluated at $b$ equals the application of the predecessor limit predicate to $b$ and the recursive function evaluated at all elements less than $b$.
PredOrder.limitRecOn_pred_of_not_isMin theorem
(hb : ¬IsMin b) : limitRecOn (Order.pred b) isMax pred isPredLimit = pred b hb (limitRecOn b isMax pred isPredLimit)
Full source 
theorem limitRecOn_pred_of_not_isMin (hb : ¬IsMin b) :
    limitRecOn (Order.pred b) isMax pred isPredLimit =
      pred b hb (limitRecOn b isMax pred isPredLimit) :=
  SuccOrder.limitRecOn_succ_of_not_isMax (α := αᵒᵈ) isMax pred _ hb
Recursion on Predecessor of Non-Minimal Elements in a Well-Founded Order
Informal description
Let $\alpha$ be a well-founded partial order with a predecessor function $\mathrm{pred}$, and let $b \in \alpha$ be a non-minimal element. Then the recursive function $\mathrm{limitRecOn}$ evaluated at $\mathrm{pred}(b)$ equals the predecessor of $b$ applied to the recursive function evaluated at $b$. In symbols: $$\mathrm{limitRecOn}(\mathrm{pred}(b)) = \mathrm{pred}(b, h_b, \mathrm{limitRecOn}(b))$$ where $h_b$ is a proof that $b$ is not minimal.
PredOrder.limitRecOn_pred theorem
[NoMinOrder α] (b : α) : limitRecOn (Order.pred b) isMax pred isPredLimit = pred b (not_isMin b) (limitRecOn b isMax pred isPredLimit)
Full source 
@[simp]
theorem limitRecOn_pred [NoMinOrder α] (b : α) :
    limitRecOn (Order.pred b) isMax pred isPredLimit =
      pred b (not_isMin b) (limitRecOn b isMax pred isPredLimit) :=
  SuccOrder.limitRecOn_succ (α := αᵒᵈ) isMax pred _ b
Recursion on Predecessor in a No-Min-Order
Informal description
Let $\alpha$ be a partial order with no minimal elements (i.e., a `NoMinOrder`). For any element $b \in \alpha$, the recursive function $\mathrm{limitRecOn}$ evaluated at the predecessor of $b$ equals the predecessor function applied to $b$ (with proof that $b$ is not minimal) and the recursive function evaluated at $b$. In symbols: $$\mathrm{limitRecOn}(\mathrm{pred}(b)) = \mathrm{pred}(b, \text{not\_isMin}(b), \mathrm{limitRecOn}(b))$$