Module docstring
{"# Archimedean successor and predecessor
IsSuccArchimedean:SuccOrderwheresucciterated to an element gives all the greater ones.IsPredArchimedean:PredOrderwhereprediterated to an element gives all the smaller ones. "}
IsSuccArchimedean
structure
(α : Type*) [Preorder α] [SuccOrder α]
Full source
/-- A `SuccOrder` is succ-archimedean if one can go from any two comparable elements by iterating
`succ` -/
class IsSuccArchimedean (α : Type*) [Preorder α] [SuccOrder α] : Prop where
/-- If `a ≤ b` then one can get to `a` from `b` by iterating `succ` -/
exists_succ_iterate_of_le {a b : α} (h : a ≤ b) : ∃ n, succ^[n] a = bInformal description
A preorder $\alpha$ equipped with a successor function is called *successor-archimedean* if for any two comparable elements $x \leq y$, there exists a natural number $n$ such that iterating the successor function $n$ times on $x$ yields an element greater than or equal to $y$. In other words, $y \leq \text{succ}^n(x)$ for some $n \in \mathbb{N}$.
IsPredArchimedean
structure
(α : Type*) [Preorder α] [PredOrder α]
Full source
/-- A `PredOrder` is pred-archimedean if one can go from any two comparable elements by iterating
`pred` -/
class IsPredArchimedean (α : Type*) [Preorder α] [PredOrder α] : Prop where
/-- If `a ≤ b` then one can get to `b` from `a` by iterating `pred` -/
exists_pred_iterate_of_le {a b : α} (h : a ≤ b) : ∃ n, pred^[n] b = aInformal description
A preorder $\alpha$ equipped with a predecessor function is called *pred-archimedean* if for any two comparable elements $a \leq b$, there exists a natural number $n$ such that iterating the predecessor function $n$ times on $b$ yields $a$. In other words, one can reach any smaller element by repeatedly applying the predecessor function.
instIsPredArchimedeanOrderDual
instance
: IsPredArchimedean αᵒᵈ
Informal description
For any preorder $\alpha$ that is successor-archimedean, its order dual $\alpha^{\mathrm{op}}$ is pred-archimedean. This means that if for any two comparable elements $x \leq y$ in $\alpha$ there exists a natural number $n$ such that $y \leq \text{succ}^n(x)$, then for any two comparable elements $a \leq b$ in $\alpha^{\mathrm{op}}$ there exists a natural number $n$ such that $\text{pred}^n(b) = a$.
LE.le.exists_succ_iterate
theorem
(h : a ≤ b) : ∃ n, succ^[n] a = b
Full source
theorem LE.le.exists_succ_iterate (h : a ≤ b) : ∃ n, succ^[n] a = b :=
exists_succ_iterate_of_le hInformal description
In a successor-archimedean order $\alpha$, for any two elements $a \leq b$, there exists a natural number $n$ such that the $n$-th iterate of the successor function applied to $a$ equals $b$, i.e., $\text{succ}^n(a) = b$.
exists_succ_iterate_iff_le
theorem
: (∃ n, succ^[n] a = b) ↔ a ≤ b
Full source
theorem exists_succ_iterate_iff_le : (∃ n, succ^[n] a = b) ↔ a ≤ b := by
refine ⟨?_, exists_succ_iterate_of_le⟩
rintro ⟨n, rfl⟩
exact id_le_iterate_of_id_le le_succ n aInformal description
For any two elements $a$ and $b$ in a successor-archimedean order $\alpha$, there exists a natural number $n$ such that the $n$-th iterate of the successor function applied to $a$ equals $b$ if and only if $a \leq b$. In other words, $\exists n, \text{succ}^n(a) = b \leftrightarrow a \leq b$.
Succ.rec
theorem
{P : α → Prop} {m : α} (h0 : P m) (h1 : ∀ n, m ≤ n → P n → P (succ n)) ⦃n : α⦄ (hmn : m ≤ n) : P n
Full source
/-- Induction principle on a type with a `SuccOrder` for all elements above a given element `m`. -/
@[elab_as_elim]
theorem Succ.rec {P : α → Prop} {m : α} (h0 : P m) (h1 : ∀ n, m ≤ n → P n → P (succ n)) ⦃n : α⦄
(hmn : m ≤ n) : P n := by
obtain ⟨n, rfl⟩ := hmn.exists_succ_iterate; clear hmn
induction' n with n ih
· exact h0
· rw [Function.iterate_succ_apply']
exact h1 _ (id_le_iterate_of_id_le le_succ n m) ihInformal description
Let $\alpha$ be a successor-archimedean order, $P$ a predicate on $\alpha$, and $m \in \alpha$ a starting element. If $P(m)$ holds, and for any $n \geq m$, $P(n)$ implies $P(\text{succ}(n))$, then $P(n)$ holds for all $n \geq m$.
Succ.rec_iff
theorem
{p : α → Prop} (hsucc : ∀ a, p a ↔ p (succ a)) {a b : α} (h : a ≤ b) : p a ↔ p b
Full source
theorem Succ.rec_iff {p : α → Prop} (hsucc : ∀ a, p a ↔ p (succ a)) {a b : α} (h : a ≤ b) :
p a ↔ p b := by
obtain ⟨n, rfl⟩ := h.exists_succ_iterate
exact Iterate.rec (fun b => p a ↔ p b) (fun c hc => hc.trans (hsucc _)) Iff.rfl nInformal description
Let $\alpha$ be a successor-archimedean order and $p : \alpha \to \text{Prop}$ a predicate such that for every $a \in \alpha$, $p(a)$ holds if and only if $p(\text{succ}(a))$ holds. Then for any two elements $a \leq b$ in $\alpha$, the predicate $p$ holds at $a$ if and only if it holds at $b$. In other words, $p(a) \leftrightarrow p(b)$ whenever $a \leq b$.
le_total_of_codirected
theorem
{r v₁ v₂ : α} (h₁ : r ≤ v₁) (h₂ : r ≤ v₂) : v₁ ≤ v₂ ∨ v₂ ≤ v₁
Full source
lemma le_total_of_codirected {r v₁ v₂ : α} (h₁ : r ≤ v₁) (h₂ : r ≤ v₂) : v₁ ≤ v₂ ∨ v₂ ≤ v₁ := by
obtain ⟨n, rfl⟩ := h₁.exists_succ_iterate
obtain ⟨m, rfl⟩ := h₂.exists_succ_iterate
clear h₁ h₂
wlog h : n ≤ m
· rw [Or.comm]
apply this
exact Nat.le_of_not_ge h
left
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
rw [Nat.add_comm, Function.iterate_add, Function.comp_apply]
apply Order.le_succ_iterateInformal description
For any elements $r, v_1, v_2$ in a preorder $\alpha$ where $r \leq v_1$ and $r \leq v_2$, either $v_1 \leq v_2$ or $v_2 \leq v_1$ holds.
instIsSuccArchimedeanOrderDual
instance
: IsSuccArchimedean αᵒᵈ
Informal description
For any preorder $\alpha$ that is pred-archimedean, its order dual $\alpha^{\mathrm{op}}$ is successor-archimedean. This means that for any two elements $x \leq y$ in $\alpha^{\mathrm{op}}$, there exists a natural number $n$ such that iterating the successor function $n$ times on $x$ yields an element greater than or equal to $y$.
LE.le.exists_pred_iterate
theorem
(h : a ≤ b) : ∃ n, pred^[n] b = a
Full source
theorem LE.le.exists_pred_iterate (h : a ≤ b) : ∃ n, pred^[n] b = a :=
exists_pred_iterate_of_le hInformal description
For any two elements $a$ and $b$ in a pred-archimedean order $\alpha$ with $a \leq b$, there exists a natural number $n$ such that the $n$-th iterate of the predecessor function evaluated at $b$ equals $a$, i.e., $\mathrm{pred}^n(b) = a$.
exists_pred_iterate_iff_le
theorem
: (∃ n, pred^[n] b = a) ↔ a ≤ b
Full source
theorem exists_pred_iterate_iff_le : (∃ n, pred^[n] b = a) ↔ a ≤ b :=
exists_succ_iterate_iff_le (α := αᵒᵈ)Informal description
For any two elements $a$ and $b$ in a pred-archimedean order $\alpha$, there exists a natural number $n$ such that the $n$-th iterate of the predecessor function applied to $b$ equals $a$ if and only if $a \leq b$. In other words, $\exists n, \mathrm{pred}^n(b) = a \leftrightarrow a \leq b$.
Pred.rec
theorem
{P : α → Prop} {m : α} (h0 : P m) (h1 : ∀ n, n ≤ m → P n → P (pred n)) ⦃n : α⦄ (hmn : n ≤ m) : P n
Informal description
Let $\alpha$ be a pred-archimedean order, $P$ a predicate on $\alpha$, and $m \in \alpha$ a starting element. If $P(m)$ holds, and for any $n \leq m$, $P(n)$ implies $P(\mathrm{pred}(n))$, then $P(n)$ holds for all $n \leq m$.
Pred.rec_iff
theorem
{p : α → Prop} (hsucc : ∀ a, p a ↔ p (pred a)) {a b : α} (h : a ≤ b) : p a ↔ p b
Full source
theorem Pred.rec_iff {p : α → Prop} (hsucc : ∀ a, p a ↔ p (pred a)) {a b : α} (h : a ≤ b) :
p a ↔ p b :=
(Succ.rec_iff (α := αᵒᵈ) hsucc h).symmInformal description
Let $\alpha$ be a pred-archimedean order and $p : \alpha \to \text{Prop}$ a predicate such that for every $a \in \alpha$, $p(a)$ holds if and only if $p(\mathrm{pred}(a))$ holds. Then for any two elements $a \leq b$ in $\alpha$, the predicate $p$ holds at $a$ if and only if it holds at $b$. In other words, $p(a) \leftrightarrow p(b)$ whenever $a \leq b$.
le_total_of_directed
theorem
{r v₁ v₂ : α} (h₁ : v₁ ≤ r) (h₂ : v₂ ≤ r) : v₁ ≤ v₂ ∨ v₂ ≤ v₁
Full source
lemma le_total_of_directed {r v₁ v₂ : α} (h₁ : v₁ ≤ r) (h₂ : v₂ ≤ r) : v₁ ≤ v₂ ∨ v₂ ≤ v₁ :=
Or.symm (le_total_of_codirected (α := αᵒᵈ) h₁ h₂)Informal description
For any elements $v_1, v_2$ in a preorder $\alpha$ that are both less than or equal to a common element $r$, either $v_1 \leq v_2$ or $v_2 \leq v_1$ holds.
lt_or_le_of_codirected
theorem
[SuccOrder α] [IsSuccArchimedean α] {r v₁ v₂ : α} (h₁ : r ≤ v₁) (h₂ : r ≤ v₂) : v₁ < v₂ ∨ v₂ ≤ v₁
Full source
lemma lt_or_le_of_codirected [SuccOrder α] [IsSuccArchimedean α] {r v₁ v₂ : α} (h₁ : r ≤ v₁)
(h₂ : r ≤ v₂) : v₁ < v₂ ∨ v₂ ≤ v₁ := by
rw [Classical.or_iff_not_imp_right]
intro nh
rcases le_total_of_codirected h₁ h₂ with h | h
· apply lt_of_le_of_ne h (ne_of_not_le nh).symm
· contradictionInformal description
Let $\alpha$ be a preorder equipped with a successor function that is successor-archimedean. For any elements $r, v_1, v_2 \in \alpha$ such that $r \leq v_1$ and $r \leq v_2$, either $v_1 < v_2$ or $v_2 \leq v_1$ holds.
IsSuccArchimedean.linearOrder
abbrev
[SuccOrder α] [IsSuccArchimedean α] [DecidableEq α] [DecidableLE α] [DecidableLT α] [IsDirected α (· ≥ ·)] :
LinearOrder α
Full source
/--
This isn't an instance due to a loop with `LinearOrder`.
-/
-- See note [reducible non instances]
abbrev IsSuccArchimedean.linearOrder [SuccOrder α] [IsSuccArchimedean α]
[DecidableEq α] [DecidableLE α] [DecidableLT α]
[IsDirected α (· ≥ ·)] : LinearOrder α where
le_total a b :=
have ⟨c, ha, hb⟩ := directed_of (· ≥ ·) a b
le_total_of_codirected ha hb
toDecidableEq := inferInstance
toDecidableLE := inferInstance
toDecidableLT := inferInstanceInformal description
Let $\alpha$ be a preorder equipped with a successor function that is successor-archimedean. If $\alpha$ has decidable equality, decidable order relations, and is directed with respect to the greater-than-or-equal-to relation, then $\alpha$ can be extended to a linear order.
lt_or_le_of_directed
theorem
[PredOrder α] [IsPredArchimedean α] {r v₁ v₂ : α} (h₁ : v₁ ≤ r) (h₂ : v₂ ≤ r) : v₁ < v₂ ∨ v₂ ≤ v₁
Full source
lemma lt_or_le_of_directed [PredOrder α] [IsPredArchimedean α] {r v₁ v₂ : α} (h₁ : v₁ ≤ r)
(h₂ : v₂ ≤ r) : v₁ < v₂ ∨ v₂ ≤ v₁ := by
rw [Classical.or_iff_not_imp_right]
intro nh
rcases le_total_of_directed h₁ h₂ with h | h
· apply lt_of_le_of_ne h (ne_of_not_le nh).symm
· contradictionInformal description
Let $\alpha$ be a preorder equipped with a predecessor function that is pred-archimedean. For any elements $v_1, v_2 \in \alpha$ such that $v_1 \leq r$ and $v_2 \leq r$ for some common upper bound $r$, either $v_1 < v_2$ or $v_2 \leq v_1$ holds.
IsPredArchimedean.linearOrder
abbrev
[PredOrder α] [IsPredArchimedean α] [DecidableEq α] [DecidableLE α] [DecidableLT α] [IsDirected α (· ≤ ·)] :
LinearOrder α
Full source
/--
This isn't an instance due to a loop with `LinearOrder`.
-/
-- See note [reducible non instances]
abbrev IsPredArchimedean.linearOrder [PredOrder α] [IsPredArchimedean α]
[DecidableEq α] [DecidableLE α] [DecidableLT α]
[IsDirected α (· ≤ ·)] : LinearOrder α :=
letI : LinearOrder αᵒᵈ := IsSuccArchimedean.linearOrder
inferInstanceAs (LinearOrder αᵒᵈαᵒᵈᵒᵈ)Informal description
Let $\alpha$ be a preorder equipped with a predecessor function that is pred-archimedean. If $\alpha$ has decidable equality, decidable order relations, and is directed with respect to the less-than-or-equal-to relation, then $\alpha$ can be extended to a linear order.
succ_max
theorem
(a b : α) : succ (max a b) = max (succ a) (succ b)
Informal description
For any two elements $a$ and $b$ in an ordered type $\alpha$ with a successor function, the successor of the maximum of $a$ and $b$ is equal to the maximum of the successors of $a$ and $b$, i.e., $\text{succ}(\max(a, b)) = \max(\text{succ}(a), \text{succ}(b))$.
succ_min
theorem
(a b : α) : succ (min a b) = min (succ a) (succ b)
Informal description
For any two elements $a$ and $b$ in an ordered type $\alpha$ with a successor function, the successor of the minimum of $a$ and $b$ is equal to the minimum of their successors, i.e., $\text{succ}(\min(a, b)) = \min(\text{succ}(a), \text{succ}(b))$.
exists_succ_iterate_or
theorem
: (∃ n, succ^[n] a = b) ∨ ∃ n, succ^[n] b = a
Full source
theorem exists_succ_iterate_or : (∃ n, succ^[n] a = b) ∨ ∃ n, succ^[n] b = a :=
(le_total a b).imp exists_succ_iterate_of_le exists_succ_iterate_of_leInformal description
For any two elements $a$ and $b$ in a successor-archimedean order $\alpha$, either there exists a natural number $n$ such that the $n$-th iterate of the successor function applied to $a$ equals $b$, or there exists a natural number $n$ such that the $n$-th iterate of the successor function applied to $b$ equals $a$. In other words, either $b$ can be reached from $a$ by iterating the successor function, or vice versa.
Succ.rec_linear
theorem
{p : α → Prop} (hsucc : ∀ a, p a ↔ p (succ a)) (a b : α) : p a ↔ p b
Full source
theorem Succ.rec_linear {p : α → Prop} (hsucc : ∀ a, p a ↔ p (succ a)) (a b : α) : p a ↔ p b :=
(le_total a b).elim (Succ.rec_iff hsucc) fun h => (Succ.rec_iff hsucc h).symmInformal description
Let $\alpha$ be a successor-archimedean order and $p : \alpha \to \text{Prop}$ a predicate such that for every $a \in \alpha$, $p(a)$ holds if and only if $p(\text{succ}(a))$ holds. Then for any two elements $a, b \in \alpha$, the predicate $p$ holds at $a$ if and only if it holds at $b$, i.e., $p(a) \leftrightarrow p(b)$.
pred_max
theorem
(a b : α) : pred (max a b) = max (pred a) (pred b)
Informal description
For any two elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessor of the maximum of $a$ and $b$ equals the maximum of their predecessors, i.e.,
\[ \mathrm{pred}(\max(a, b)) = \max(\mathrm{pred}(a), \mathrm{pred}(b)). \]
pred_min
theorem
(a b : α) : pred (min a b) = min (pred a) (pred b)
Informal description
For any two elements $a$ and $b$ in a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$, the predecessor of the minimum of $a$ and $b$ equals the minimum of their predecessors, i.e., $\mathrm{pred}(\min(a, b)) = \min(\mathrm{pred}(a), \mathrm{pred}(b))$.
exists_pred_iterate_or
theorem
: (∃ n, pred^[n] b = a) ∨ ∃ n, pred^[n] a = b
Full source
theorem exists_pred_iterate_or : (∃ n, pred^[n] b = a) ∨ ∃ n, pred^[n] a = b :=
(le_total a b).imp exists_pred_iterate_of_le exists_pred_iterate_of_leInformal description
For any two elements $a$ and $b$ in a pred-archimedean order $\alpha$, either there exists a natural number $n$ such that the $n$-th iterate of the predecessor function on $b$ equals $a$, or there exists a natural number $n$ such that the $n$-th iterate of the predecessor function on $a$ equals $b$.
Pred.rec_linear
theorem
{p : α → Prop} (hsucc : ∀ a, p a ↔ p (pred a)) (a b : α) : p a ↔ p b
Full source
theorem Pred.rec_linear {p : α → Prop} (hsucc : ∀ a, p a ↔ p (pred a)) (a b : α) : p a ↔ p b :=
(le_total a b).elim (Pred.rec_iff hsucc) fun h => (Pred.rec_iff hsucc h).symmInformal description
Let $\alpha$ be a pred-archimedean order and $p : \alpha \to \text{Prop}$ a predicate such that for every $a \in \alpha$, $p(a)$ holds if and only if $p(\mathrm{pred}(a))$ holds. Then for any two elements $a, b \in \alpha$, the predicate $p$ holds at $a$ if and only if it holds at $b$. In other words, $p(a) \leftrightarrow p(b)$ for all $a, b \in \alpha$.
StrictMono.not_bddAbove_range_of_isSuccArchimedean
theorem
[NoMaxOrder α] [SuccOrder β] [IsSuccArchimedean β] (hf : StrictMono f) : ¬BddAbove (Set.range f)
Full source
lemma StrictMono.not_bddAbove_range_of_isSuccArchimedean [NoMaxOrder α] [SuccOrder β]
[IsSuccArchimedean β] (hf : StrictMono f) : ¬ BddAbove (Set.range f) := by
rintro ⟨m, hm⟩
have hm' : ∀ a, f a ≤ m := fun a ↦ hm <| Set.mem_range_self _
obtain ⟨a₀⟩ := ‹Nonempty α›
suffices ∀ b, f a₀ ≤ b → ∃ a, b < f a by
obtain ⟨a, ha⟩ : ∃ a, m < f a := this m (hm' a₀)
exact ha.not_le (hm' a)
have h : ∀ a, ∃ a', f a < f a' := fun a ↦ (exists_gt a).imp (fun a' h ↦ hf h)
apply Succ.rec
· exact h a₀
rintro b _ ⟨a, hba⟩
exact (h a).imp (fun a' ↦ (succ_le_of_lt hba).trans_lt)Informal description
Let $\alpha$ be an order with no maximal element, and $\beta$ a successor-archimedean order equipped with a successor function. If $f : \alpha \to \beta$ is a strictly monotone function, then the range of $f$ is not bounded above in $\beta$.
StrictMono.not_bddBelow_range_of_isPredArchimedean
theorem
[NoMinOrder α] [PredOrder β] [IsPredArchimedean β] (hf : StrictMono f) : ¬BddBelow (Set.range f)
Full source
lemma StrictMono.not_bddBelow_range_of_isPredArchimedean [NoMinOrder α] [PredOrder β]
[IsPredArchimedean β] (hf : StrictMono f) : ¬ BddBelow (Set.range f) :=
hf.dual.not_bddAbove_range_of_isSuccArchimedeanInformal description
Let $\alpha$ be an order with no minimal element, and $\beta$ a pred-archimedean order equipped with a predecessor function. If $f : \alpha \to \beta$ is a strictly monotone function, then the range of $f$ is not bounded below in $\beta$.
StrictAnti.not_bddBelow_range_of_isSuccArchimedean
theorem
[NoMinOrder α] [SuccOrder β] [IsSuccArchimedean β] (hf : StrictAnti f) : ¬BddAbove (Set.range f)
Full source
lemma StrictAnti.not_bddBelow_range_of_isSuccArchimedean [NoMinOrder α] [SuccOrder β]
[IsSuccArchimedean β] (hf : StrictAnti f) : ¬ BddAbove (Set.range f) :=
hf.dual_right.not_bddBelow_range_of_isPredArchimedeanInformal description
Let $\alpha$ be an order with no minimal element, and $\beta$ a successor-archimedean order equipped with a successor function. If $f : \alpha \to \beta$ is a strictly antitone function, then the range of $f$ is not bounded above in $\beta$.
StrictAnti.not_bddBelow_range_of_isPredArchimedean
theorem
[NoMaxOrder α] [PredOrder β] [IsPredArchimedean β] (hf : StrictAnti f) : ¬BddBelow (Set.range f)
Full source
lemma StrictAnti.not_bddBelow_range_of_isPredArchimedean [NoMaxOrder α] [PredOrder β]
[IsPredArchimedean β] (hf : StrictAnti f) : ¬ BddBelow (Set.range f) :=
hf.dual_right.not_bddAbove_range_of_isSuccArchimedeanInformal description
Let $\alpha$ be an order with no maximal element, and $\beta$ a pred-archimedean order equipped with a predecessor function. If $f : \alpha \to \beta$ is a strictly antitone function, then the range of $f$ is not bounded below in $\beta$.
WellFoundedLT.toIsPredArchimedean
instance
[h : WellFoundedLT α] [PredOrder α] : IsPredArchimedean α
Full source
instance (priority := 100) WellFoundedLT.toIsPredArchimedean [h : WellFoundedLT α]
[PredOrder α] : IsPredArchimedean α :=
⟨fun {a b} => by
refine WellFounded.fix (C := fun b => a ≤ b → ∃ n, Nat.iterate pred n b = a)
h.wf ?_ b
intros b ih hab
replace hab := eq_or_lt_of_le hab
rcases hab with (rfl | hab)
· exact ⟨0, rfl⟩
rcases eq_or_lt_of_le (pred_le b) with hb | hb
· cases (min_of_le_pred hb.ge).not_lt hab
dsimp at ih
obtain ⟨k, hk⟩ := ih (pred b) hb (le_pred_of_lt hab)
refine ⟨k + 1, ?_⟩
rw [iterate_add_apply, iterate_one, hk]⟩Informal description
For any preorder $\alpha$ with a well-founded strict less-than relation and equipped with a predecessor function, $\alpha$ is pred-archimedean. This means that for any two comparable elements $a \leq b$, there exists a natural number $n$ such that iterating the predecessor function $n$ times on $b$ yields $a$.
WellFoundedGT.toIsSuccArchimedean
instance
[h : WellFoundedGT α] [SuccOrder α] : IsSuccArchimedean α
Full source
instance (priority := 100) WellFoundedGT.toIsSuccArchimedean [h : WellFoundedGT α]
[SuccOrder α] : IsSuccArchimedean α :=
let h : IsPredArchimedean αᵒᵈ := by infer_instance
⟨h.1⟩Informal description
For any preorder $\alpha$ with a well-founded strict greater-than relation and equipped with a successor function, $\alpha$ is successor-archimedean. This means that for any two comparable elements $x \leq y$, there exists a natural number $n$ such that iterating the successor function $n$ times on $x$ yields an element greater than or equal to $y$.
Succ.rec_bot
theorem
(p : α → Prop) (hbot : p ⊥) (hsucc : ∀ a, p a → p (succ a)) (a : α) : p a
Informal description
Let $\alpha$ be a successor-archimedean order with a bottom element $\bot$, and let $P$ be a predicate on $\alpha$. If $P(\bot)$ holds and for any element $a \in \alpha$, $P(a)$ implies $P(\text{succ}(a))$, then $P(a)$ holds for all $a \in \alpha$.
Pred.rec_top
theorem
(p : α → Prop) (htop : p ⊤) (hpred : ∀ a, p a → p (pred a)) (a : α) : p a
Informal description
Let $\alpha$ be a pred-archimedean order with a top element $\top$, and let $P$ be a predicate on $\alpha$. If $P(\top)$ holds and for any element $a \in \alpha$, $P(a)$ implies $P(\mathrm{pred}(a))$, then $P(a)$ holds for all $a \in \alpha$.
SuccOrder.forall_ne_bot_iff
theorem
[Nontrivial α] [PartialOrder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α] (P : α → Prop) :
(∀ i, i ≠ ⊥ → P i) ↔ (∀ i, P (SuccOrder.succ i))
Full source
lemma SuccOrder.forall_ne_bot_iff
[Nontrivial α] [PartialOrder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α]
(P : α → Prop) :
(∀ i, i ≠ ⊥ → P i) ↔ (∀ i, P (SuccOrder.succ i)) := by
refine ⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ ?_⟩
obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i)
have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose! hi; simp [hi]
rw [← Nat.succ_pred_eq_of_pos hj]
simp only [Function.iterate_succ', Function.comp_apply]
apply hInformal description
Let $\alpha$ be a nontrivial partially ordered set with a bottom element $\bot$, equipped with a successor function and satisfying the successor-archimedean property. For any predicate $P$ on $\alpha$, the following are equivalent:
1. For every element $i \in \alpha$ with $i \neq \bot$, $P(i)$ holds.
2. For every element $i \in \alpha$, $P(\mathrm{succ}(i))$ holds.
BddAbove.exists_isGreatest_of_nonempty
theorem
{X : Type*} [LinearOrder X] [SuccOrder X] [IsSuccArchimedean X] {S : Set X} (hS : BddAbove S) (hS' : S.Nonempty) :
∃ x, IsGreatest S x
Full source
lemma BddAbove.exists_isGreatest_of_nonempty {X : Type*} [LinearOrder X] [SuccOrder X]
[IsSuccArchimedean X] {S : Set X} (hS : BddAbove S) (hS' : S.Nonempty) :
∃ x, IsGreatest S x := by
obtain ⟨m, hm⟩ := hS
obtain ⟨n, hn⟩ := hS'
by_cases hm' : m ∈ S
· exact ⟨_, hm', hm⟩
have hn' := hm hn
revert hn hm hm'
refine Succ.rec ?_ ?_ hn'
· simp +contextual
intro m _ IH hm hn hm'
rw [mem_upperBounds] at IH hm
simp_rw [Order.le_succ_iff_eq_or_le] at hm
replace hm : ∀ x ∈ S, x ≤ m := by
intro x hx
refine (hm x hx).resolve_left ?_
rintro rfl
exact hm' hx
by_cases hmS : m ∈ S
· exact ⟨m, hmS, hm⟩
· exact IH hm hn hmSInformal description
Let $X$ be a linearly ordered set equipped with a successor function and satisfying the successor-archimedean property. For any nonempty subset $S \subseteq X$ that is bounded above, there exists a greatest element in $S$.
BddBelow.exists_isLeast_of_nonempty
theorem
{X : Type*} [LinearOrder X] [PredOrder X] [IsPredArchimedean X] {S : Set X} (hS : BddBelow S) (hS' : S.Nonempty) :
∃ x, IsLeast S x
Full source
lemma BddBelow.exists_isLeast_of_nonempty {X : Type*} [LinearOrder X] [PredOrder X]
[IsPredArchimedean X] {S : Set X} (hS : BddBelow S) (hS' : S.Nonempty) :
∃ x, IsLeast S x :=
hS.dual.exists_isGreatest_of_nonempty hS'Informal description
Let $X$ be a linearly ordered set equipped with a predecessor function and satisfying the pred-archimedean property. For any nonempty subset $S \subseteq X$ that is bounded below, there exists a least element in $S$.
IsSuccArchimedean.of_orderIso
theorem
[SuccOrder X] [IsSuccArchimedean X] [SuccOrder Y] (f : X ≃o Y) : IsSuccArchimedean Y
Full source
/-- `IsSuccArchimedean` transfers across equivalences between `SuccOrder`s. -/
protected lemma IsSuccArchimedean.of_orderIso [SuccOrder X] [IsSuccArchimedean X] [SuccOrder Y]
(f : X ≃o Y) : IsSuccArchimedean Y where
exists_succ_iterate_of_le {a b} h := by
refine (exists_succ_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_
intro n
rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]
rintro rfl
clear h
induction n generalizing a with
| zero => simp
| succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]Informal description
Let $X$ and $Y$ be preorders equipped with successor functions, and let $f : X \simeq Y$ be an order isomorphism. If $X$ is successor-archimedean, then $Y$ is also successor-archimedean.
IsPredArchimedean.of_orderIso
theorem
[PredOrder X] [IsPredArchimedean X] [PredOrder Y] (f : X ≃o Y) : IsPredArchimedean Y
Full source
/-- `IsPredArchimedean` transfers across equivalences between `PredOrder`s. -/
protected lemma IsPredArchimedean.of_orderIso [PredOrder X] [IsPredArchimedean X] [PredOrder Y]
(f : X ≃o Y) : IsPredArchimedean Y where
exists_pred_iterate_of_le {a b} h := by
refine (exists_pred_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_
intro n
rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]
rintro rfl
clear h
induction n generalizing b with
| zero => simp
| succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_pred]Informal description
Let $X$ and $Y$ be preorders equipped with predecessor functions, and let $f : X \simeq Y$ be an order isomorphism. If $X$ is pred-archimedean, then $Y$ is also pred-archimedean.
Set.OrdConnected.isPredArchimedean
instance
[PredOrder α] [IsPredArchimedean α] (s : Set α) [s.OrdConnected] : IsPredArchimedean s
Full source
instance Set.OrdConnected.isPredArchimedean [PredOrder α] [IsPredArchimedean α]
(s : Set α) [s.OrdConnected] : IsPredArchimedean s where
exists_pred_iterate_of_le := @fun ⟨b, hb⟩ ⟨c, hc⟩ hbc ↦ by classical
simp only [Subtype.mk_le_mk] at hbc
obtain ⟨n, hn⟩ := hbc.exists_pred_iterate
use n
induction n generalizing c with
| zero => simp_all
| succ n hi =>
simp_all only [Function.iterate_succ, Function.comp_apply]
change Order.predOrder.pred^[n] (dite ..) = _
split_ifs with h
· dsimp only at h ⊢
apply hi _ _ _ hn
· rw [← hn]
apply Order.pred_iterate_le
· have : Order.pred (⟨c, hc⟩ : s) = ⟨c, hc⟩ := by
change dite .. = _
simp [h]
rw [Function.iterate_fixed]
· simp only [Order.pred_eq_iff_isMin] at this
apply (this.eq_of_le _).symm
exact hbc
· exact thisInformal description
For any subset $s$ of a pred-archimedean order $\alpha$ that is order-connected (i.e., for any $x, y \in s$, the interval $[x, y]$ is contained in $s$), the subset $s$ inherits the pred-archimedean property from $\alpha$. This means that for any two elements $a \leq b$ in $s$, there exists a natural number $n$ such that the $n$-th iterate of the predecessor function evaluated at $b$ equals $a$, i.e., $\mathrm{pred}^n(b) = a$.
Set.OrdConnected.isSuccArchimedean
instance
[SuccOrder α] [IsSuccArchimedean α] (s : Set α) [s.OrdConnected] : IsSuccArchimedean s
Full source
instance Set.OrdConnected.isSuccArchimedean [SuccOrder α] [IsSuccArchimedean α]
(s : Set α) [s.OrdConnected] : IsSuccArchimedean s :=
letI : IsPredArchimedean sᵒᵈ := inferInstanceAs (IsPredArchimedean (OrderDual.ofDualOrderDual.ofDual ⁻¹' s))
inferInstanceAs (IsSuccArchimedean sᵒᵈsᵒᵈᵒᵈ)Informal description
For any order-connected subset $s$ of a successor-archimedean preorder $\alpha$, the subset $s$ inherits the successor-archimedean property. This means that for any two comparable elements $x \leq y$ in $s$, there exists a natural number $n$ such that iterating the successor function $n$ times on $x$ yields an element greater than or equal to $y$.
monotoneOn_of_le_succ
theorem
(hs : s.OrdConnected) (hf : ∀ a, ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)) : MonotoneOn f s
Full source
lemma monotoneOn_of_le_succ (hs : s.OrdConnected)
(hf : ∀ a, ¬ IsMax a → a ∈ s → succsucc a ∈ s → f a ≤ f (succ a)) : MonotoneOn f s := by
rintro a ha b hb hab
obtain ⟨n, rfl⟩ := exists_succ_iterate_of_le hab
clear hab
induction' n with n hn
· simp
rw [Function.iterate_succ_apply'] at hb ⊢
have : succsucc^[n]succ^[n] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
by_cases hb' : IsMax (succ^[n] a)
· rw [succ_eq_iff_isMax.2 hb']
exact hn this
· exact (hn this).trans (hf _ hb' this hb)Informal description
Let $s$ be an order-connected subset of a preorder $\alpha$ equipped with a successor function. If for every non-maximal element $a \in s$ such that $\text{succ}(a) \in s$, the inequality $f(a) \leq f(\text{succ}(a))$ holds, then the function $f$ is monotone on $s$.
antitoneOn_of_succ_le
theorem
(hs : s.OrdConnected) (hf : ∀ a, ¬IsMax a → a ∈ s → succ a ∈ s → f (succ a) ≤ f a) : AntitoneOn f s
Full source
lemma antitoneOn_of_succ_le (hs : s.OrdConnected)
(hf : ∀ a, ¬ IsMax a → a ∈ s → succsucc a ∈ s → f (succ a) ≤ f a) : AntitoneOn f s :=
monotoneOn_of_le_succ (β := βᵒᵈ) hs hfInformal description
Let $s$ be an order-connected subset of a preorder $\alpha$ equipped with a successor function. If for every non-maximal element $a \in s$ such that $\text{succ}(a) \in s$, the inequality $f(\text{succ}(a)) \leq f(a)$ holds, then the function $f$ is antitone on $s$.
strictMonoOn_of_lt_succ
theorem
(hs : s.OrdConnected) (hf : ∀ a, ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)) : StrictMonoOn f s
Full source
lemma strictMonoOn_of_lt_succ (hs : s.OrdConnected)
(hf : ∀ a, ¬ IsMax a → a ∈ s → succsucc a ∈ s → f a < f (succ a)) : StrictMonoOn f s := by
rintro a ha b hb hab
obtain ⟨n, rfl⟩ := exists_succ_iterate_of_le hab.le
obtain _ | n := n
· simp at hab
apply not_isMax_of_lt at hab
induction' n with n hn
· simpa using hf _ hab ha hb
rw [Function.iterate_succ_apply'] at hb ⊢
have : succsucc^[n + 1]succ^[n + 1] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
by_cases hb' : IsMax (succ^[n + 1] a)
· rw [succ_eq_iff_isMax.2 hb']
exact hn this
· exact (hn this).trans (hf _ hb' this hb)Informal description
Let $s$ be an order connected subset of a preorder $\alpha$ equipped with a successor function. If for every non-maximal element $a \in s$ such that $\text{succ}(a) \in s$, we have $f(a) < f(\text{succ}(a))$, then $f$ is strictly monotone on $s$.
strictAntiOn_of_succ_lt
theorem
(hs : s.OrdConnected) (hf : ∀ a, ¬IsMax a → a ∈ s → succ a ∈ s → f (succ a) < f a) : StrictAntiOn f s
Full source
lemma strictAntiOn_of_succ_lt (hs : s.OrdConnected)
(hf : ∀ a, ¬ IsMax a → a ∈ s → succsucc a ∈ s → f (succ a) < f a) : StrictAntiOn f s :=
strictMonoOn_of_lt_succ (β := βᵒᵈ) hs hfInformal description
Let $s$ be an order-connected subset of a preorder $\alpha$ equipped with a successor function. If for every non-maximal element $a \in s$ such that $\text{succ}(a) \in s$, we have $f(\text{succ}(a)) < f(a)$, then $f$ is strictly antitone on $s$.
monotone_of_le_succ
theorem
(hf : ∀ a, ¬IsMax a → f a ≤ f (succ a)) : Monotone f
Full source
lemma monotone_of_le_succ (hf : ∀ a, ¬ IsMax a → f a ≤ f (succ a)) : Monotone f := by
simpa using monotoneOn_of_le_succ Set.ordConnected_univ (by simpa using hf)Informal description
Let $f$ be a function defined on a preorder $\alpha$ equipped with a successor function. If for every non-maximal element $a \in \alpha$, the inequality $f(a) \leq f(\text{succ}(a))$ holds, then $f$ is monotone on $\alpha$.
antitone_of_succ_le
theorem
(hf : ∀ a, ¬IsMax a → f (succ a) ≤ f a) : Antitone f
Full source
lemma antitone_of_succ_le (hf : ∀ a, ¬ IsMax a → f (succ a) ≤ f a) : Antitone f := by
simpa using antitoneOn_of_succ_le Set.ordConnected_univ (by simpa using hf)Informal description
Let $f$ be a function defined on a preorder $\alpha$ equipped with a successor function. If for every non-maximal element $a \in \alpha$, the inequality $f(\text{succ}(a)) \leq f(a)$ holds, then $f$ is antitone on $\alpha$.
strictMono_of_lt_succ
theorem
(hf : ∀ a, ¬IsMax a → f a < f (succ a)) : StrictMono f
Full source
lemma strictMono_of_lt_succ (hf : ∀ a, ¬ IsMax a → f a < f (succ a)) : StrictMono f := by
simpa using strictMonoOn_of_lt_succ Set.ordConnected_univ (by simpa using hf)Informal description
Let $f$ be a function on a preorder $\alpha$ equipped with a successor function. If for every non-maximal element $a \in \alpha$, we have $f(a) < f(\text{succ}(a))$, then $f$ is strictly monotone.
strictAnti_of_succ_lt
theorem
(hf : ∀ a, ¬IsMax a → f (succ a) < f a) : StrictAnti f
Full source
lemma strictAnti_of_succ_lt (hf : ∀ a, ¬ IsMax a → f (succ a) < f a) : StrictAnti f := by
simpa using strictAntiOn_of_succ_lt Set.ordConnected_univ (by simpa using hf)Informal description
Let $f$ be a function on a preorder $\alpha$ equipped with a successor function. If for every non-maximal element $a \in \alpha$, the value of $f$ at the successor of $a$ is strictly less than the value at $a$ (i.e., $f(\text{succ}(a)) < f(a)$), then $f$ is strictly antitone on $\alpha$.
monotoneOn_of_pred_le
theorem
(hs : s.OrdConnected) (hf : ∀ a, ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a) : MonotoneOn f s
Full source
lemma monotoneOn_of_pred_le (hs : s.OrdConnected)
(hf : ∀ a, ¬ IsMin a → a ∈ s → predpred a ∈ s → f (pred a) ≤ f a) : MonotoneOn f s := by
rintro a ha b hb hab
obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab
clear hab
induction' n with n hn
· simp
rw [Function.iterate_succ_apply'] at ha ⊢
have : predpred^[n]pred^[n] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
by_cases ha' : IsMin (pred^[n] b)
· rw [pred_eq_iff_isMin.2 ha']
exact hn this
· exact (hn this).trans' (hf _ ha' this ha)Informal description
Let $s$ be an order-connected subset of a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$. If for every non-minimal element $a \in s$ such that $\mathrm{pred}(a) \in s$, we have $f(\mathrm{pred}(a)) \leq f(a)$, then the function $f$ is monotone on $s$.
antitoneOn_of_le_pred
theorem
(hs : s.OrdConnected) (hf : ∀ a, ¬IsMin a → a ∈ s → pred a ∈ s → f a ≤ f (pred a)) : AntitoneOn f s
Full source
lemma antitoneOn_of_le_pred (hs : s.OrdConnected)
(hf : ∀ a, ¬ IsMin a → a ∈ s → predpred a ∈ s → f a ≤ f (pred a)) : AntitoneOn f s :=
monotoneOn_of_pred_le (β := βᵒᵈ) hs hfInformal description
Let $s$ be an order-connected subset of a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$. If for every non-minimal element $a \in s$ such that $\mathrm{pred}(a) \in s$, the function $f$ satisfies $f(a) \leq f(\mathrm{pred}(a))$, then $f$ is antitone on $s$.
strictMonoOn_of_pred_lt
theorem
(hs : s.OrdConnected) (hf : ∀ a, ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a) : StrictMonoOn f s
Full source
lemma strictMonoOn_of_pred_lt (hs : s.OrdConnected)
(hf : ∀ a, ¬ IsMin a → a ∈ s → predpred a ∈ s → f (pred a) < f a) : StrictMonoOn f s := by
rintro a ha b hb hab
obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab.le
obtain _ | n := n
· simp at hab
apply not_isMin_of_lt at hab
induction' n with n hn
· simpa using hf _ hab hb ha
rw [Function.iterate_succ_apply'] at ha ⊢
have : predpred^[n + 1]pred^[n + 1] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
by_cases ha' : IsMin (pred^[n + 1] b)
· rw [pred_eq_iff_isMin.2 ha']
exact hn this
· exact (hn this).trans' (hf _ ha' this ha)Informal description
Let $s$ be an order connected subset of a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$. If for every non-minimal element $a \in s$ such that $\mathrm{pred}(a) \in s$, the function $f$ satisfies $f(\mathrm{pred}(a)) < f(a)$, then $f$ is strictly monotone on $s$.
strictAntiOn_of_lt_pred
theorem
(hs : s.OrdConnected) (hf : ∀ a, ¬IsMin a → a ∈ s → pred a ∈ s → f a < f (pred a)) : StrictAntiOn f s
Full source
lemma strictAntiOn_of_lt_pred (hs : s.OrdConnected)
(hf : ∀ a, ¬ IsMin a → a ∈ s → predpred a ∈ s → f a < f (pred a)) : StrictAntiOn f s :=
strictMonoOn_of_pred_lt (β := βᵒᵈ) hs hfInformal description
Let $s$ be an order connected subset of a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$. If for every non-minimal element $a \in s$ such that $\mathrm{pred}(a) \in s$, the function $f$ satisfies $f(a) < f(\mathrm{pred}(a))$, then $f$ is strictly antitone on $s$.
monotone_of_pred_le
theorem
(hf : ∀ a, ¬IsMin a → f (pred a) ≤ f a) : Monotone f
Full source
lemma monotone_of_pred_le (hf : ∀ a, ¬ IsMin a → f (pred a) ≤ f a) : Monotone f := by
simpa using monotoneOn_of_pred_le Set.ordConnected_univ (by simpa using hf)Informal description
Let $\alpha$ be a preorder equipped with a predecessor function $\mathrm{pred}$. If for every non-minimal element $a \in \alpha$, the function $f$ satisfies $f(\mathrm{pred}(a)) \leq f(a)$, then $f$ is monotone on $\alpha$.
antitone_of_le_pred
theorem
(hf : ∀ a, ¬IsMin a → f a ≤ f (pred a)) : Antitone f
Full source
lemma antitone_of_le_pred (hf : ∀ a, ¬ IsMin a → f a ≤ f (pred a)) : Antitone f := by
simpa using antitoneOn_of_le_pred Set.ordConnected_univ (by simpa using hf)Informal description
Let $\alpha$ be a preorder equipped with a predecessor function $\mathrm{pred}$. If a function $f : \alpha \to \alpha$ satisfies $f(a) \leq f(\mathrm{pred}(a))$ for every non-minimal element $a \in \alpha$, then $f$ is antitone on $\alpha$.
strictMono_of_pred_lt
theorem
(hf : ∀ a, ¬IsMin a → f (pred a) < f a) : StrictMono f
Full source
lemma strictMono_of_pred_lt (hf : ∀ a, ¬ IsMin a → f (pred a) < f a) : StrictMono f := by
simpa using strictMonoOn_of_pred_lt Set.ordConnected_univ (by simpa using hf)Informal description
Let $f$ be a function on a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$. If for every non-minimal element $a \in \alpha$, the function $f$ satisfies $f(\mathrm{pred}(a)) < f(a)$, then $f$ is strictly monotone on $\alpha$.
strictAnti_of_lt_pred
theorem
(hf : ∀ a, ¬IsMin a → f a < f (pred a)) : StrictAnti f
Full source
lemma strictAnti_of_lt_pred (hf : ∀ a, ¬ IsMin a → f a < f (pred a)) : StrictAnti f := by
simpa using strictAntiOn_of_lt_pred Set.ordConnected_univ (by simpa using hf)Informal description
Let $f$ be a function on a preorder $\alpha$ equipped with a predecessor function $\mathrm{pred}$. If for every non-minimal element $a \in \alpha$, the function $f$ satisfies $f(a) < f(\mathrm{pred}(a))$, then $f$ is strictly antitone on $\alpha$.