Mathlib.Algebra.Order.SuccPred

SuccAddOrder structure

(α : Type*) [Preorder α] [Add α] [One α] extends SuccOrder α

Full source

/-- A typeclass for `succ x = x + 1`. -/
class SuccAddOrder (α : Type*) [Preorder α] [Add α] [One α] extends SuccOrder α where
  succ_eq_add_one (x : α) : succ x = x + 1

Successor as addition by one

Informal description

A structure `SuccAddOrder` on a type `α` with a preorder, addition, and a distinguished element `1` extends the `SuccOrder` structure, ensuring that the successor function satisfies `succ x = x + 1` for all `x ∈ α`.

PredSubOrder structure

(α : Type*) [Preorder α] [Sub α] [One α] extends PredOrder α

Full source

/-- A typeclass for `pred x = x - 1`. -/
class PredSubOrder (α : Type*) [Preorder α] [Sub α] [One α] extends PredOrder α where
  pred_eq_sub_one (x : α) : pred x = x - 1

Predecessor as subtraction by one

Informal description

A structure `PredSubOrder` for a type $\alpha$ with a preorder, subtraction, and a distinguished element $1$, extending `PredOrder`, where the predecessor function satisfies $\mathrm{pred}(x) = x - 1$ for all $x \in \alpha$.

Order.succ_eq_add_one theorem

(x : α) : succ x = x + 1

Full source

theorem succ_eq_add_one (x : α) : succ x = x + 1 :=
  SuccAddOrder.succ_eq_add_one x

Successor as Addition by One: $\mathrm{succ}(x) = x + 1$

Informal description

For any element $x$ in a type $\alpha$ equipped with a preorder, addition, and a distinguished element $1$, the successor of $x$ is equal to $x + 1$.

Order.add_one_le_of_lt theorem

(h : x < y) : x + 1 ≤ y

Full source

theorem add_one_le_of_lt (h : x < y) : x + 1 ≤ y := by
  rw [← succ_eq_add_one]
  exact succ_le_of_lt h

Addition of One Preserves Strict Inequality in Ordered Types

Informal description

For any elements $x$ and $y$ in a preorder $\alpha$ with addition and a distinguished element $1$, if $x < y$, then $x + 1 \leq y$.

Order.add_one_le_iff_of_not_isMax theorem

(hx : ¬IsMax x) : x + 1 ≤ y ↔ x < y

Full source

theorem add_one_le_iff_of_not_isMax (hx : ¬ IsMax x) : x + 1 ≤ y ↔ x < y := by
  rw [← succ_eq_add_one, succ_le_iff_of_not_isMax hx]

Characterization of Addition by One for Non-Maximal Elements: $x + 1 \leq y \leftrightarrow x < y$

Informal description

For any element $x$ in a preorder $\alpha$ with addition and a distinguished element $1$, if $x$ is not maximal, then $x + 1 \leq y$ if and only if $x < y$.

Order.add_one_le_iff theorem

[NoMaxOrder α] : x + 1 ≤ y ↔ x < y

Full source

theorem add_one_le_iff [NoMaxOrder α] : x + 1 ≤ y ↔ x < y :=
  add_one_le_iff_of_not_isMax (not_isMax x)

Characterization of Addition by One in Orders without Maximal Elements: $x + 1 \leq y \leftrightarrow x < y$

Informal description

In a preorder $\alpha$ with no maximal elements, for any elements $x$ and $y$, the inequality $x + 1 \leq y$ holds if and only if $x < y$.

Order.wcovBy_add_one theorem

(x : α) : x ⩿ x + 1

Full source

@[simp]
theorem wcovBy_add_one (x : α) : x ⩿ x + 1 := by
  rw [← succ_eq_add_one]
  exact wcovBy_succ x

Weak Covering Property of Addition by One: $x \ ⩿ \ x + 1$

Informal description

For any element $x$ in a type $\alpha$ equipped with a preorder, addition, and a distinguished element $1$, the element $x$ is weakly covered by $x + 1$, i.e., $x \ ⩿ \ x + 1$. This means that $x \leq x + 1$ and there is no element strictly between $x$ and $x + 1$.

Order.covBy_add_one theorem

[NoMaxOrder α] (x : α) : x ⋖ x + 1

Full source

@[simp]
theorem covBy_add_one [NoMaxOrder α] (x : α) : x ⋖ x + 1 := by
  rw [← succ_eq_add_one]
  exact covBy_succ x

Covering property of addition by one: $x \lessdot x + 1$

Informal description

For any element $x$ in a type $\alpha$ with no maximal elements, the element $x$ is covered by $x + 1$, i.e., $x \lessdot x + 1$. This means that $x < x + 1$ and there is no element strictly between $x$ and $x + 1$.

Order.pred_eq_sub_one theorem

(x : α) : pred x = x - 1

Full source

theorem pred_eq_sub_one (x : α) : pred x = x - 1 :=
  PredSubOrder.pred_eq_sub_one x

Predecessor as Subtraction by One

Informal description

For any element $x$ in a type $\alpha$ equipped with a preorder, subtraction, and a `PredSubOrder` structure, the predecessor of $x$ equals $x$ minus one, i.e., $\mathrm{pred}(x) = x - 1$.

Order.le_sub_one_of_lt theorem

(h : x < y) : x ≤ y - 1

Full source

theorem le_sub_one_of_lt (h : x < y) : x ≤ y - 1 := by
  rw [← pred_eq_sub_one]
  exact le_pred_of_lt h

Inequality implies less than or equal to predecessor: $x < y \to x \leq y - 1$

Informal description

For any elements $x$ and $y$ in a preorder $\alpha$ equipped with subtraction and a distinguished element $1$, if $x < y$, then $x$ is less than or equal to $y - 1$.

Order.le_sub_one_iff_of_not_isMin theorem

(hy : ¬IsMin y) : x ≤ y - 1 ↔ x < y

Full source

theorem le_sub_one_iff_of_not_isMin (hy : ¬ IsMin y) : x ≤ y - 1 ↔ x < y := by
  rw [← pred_eq_sub_one, le_pred_iff_of_not_isMin hy]

Characterization of Predecessor Inequality for Non-Minimal Elements: $x \leq y - 1 \leftrightarrow x < y$

Informal description

For any elements $x$ and $y$ in a preorder $\alpha$ equipped with subtraction and a distinguished element $1$, if $y$ is not minimal, then $x \leq y - 1$ if and only if $x < y$.

Order.le_sub_one_iff theorem

[NoMinOrder α] : x ≤ y - 1 ↔ x < y

Full source

theorem le_sub_one_iff [NoMinOrder α] : x ≤ y - 1 ↔ x < y :=
  le_sub_one_iff_of_not_isMin (not_isMin y)

Characterization of Predecessor Inequality in Orders without Minimal Elements: $x \leq y - 1 \leftrightarrow x < y$

Informal description

For any elements $x$ and $y$ in a preorder $\alpha$ with no minimal elements and equipped with subtraction and a distinguished element $1$, the inequality $x \leq y - 1$ holds if and only if $x < y$.

Order.sub_one_wcovBy theorem

(x : α) : x - 1 ⩿ x

Full source

@[simp]
theorem sub_one_wcovBy (x : α) : x - 1 ⩿ x := by
  rw [← pred_eq_sub_one]
  exact pred_wcovBy x

Weak covering relation for predecessor: $x - 1 \ ⩿ \ x$

Informal description

For any element $x$ in a preorder $\alpha$ equipped with subtraction and a `PredSubOrder` structure, the element $x - 1$ weakly covers $x$, i.e., $x - 1 \ ⩿ \ x$.

Order.sub_one_covBy theorem

[NoMinOrder α] (x : α) : x - 1 ⋖ x

Full source

@[simp]
theorem sub_one_covBy [NoMinOrder α] (x : α) : x - 1 ⋖ x := by
  rw [← pred_eq_sub_one]
  exact pred_covBy x

Covering relation for predecessor: $x - 1 \lessdot x$ in orders without minimal elements

Informal description

For any element $x$ in a preorder $\alpha$ with no minimal elements and equipped with subtraction and a `PredSubOrder` structure, the element $x - 1$ is covered by $x$, i.e., $x - 1 \lessdot x$.

Order.succ_iterate theorem

[AddMonoidWithOne α] [SuccAddOrder α] (x : α) (n : ℕ) : succ^[n] x = x + n

Full source

@[simp]
theorem succ_iterate [AddMonoidWithOne α] [SuccAddOrder α] (x : α) (n : ℕ) :
    succsucc^[n] x = x + n := by
  induction n with
  | zero =>
    rw [Function.iterate_zero_apply, Nat.cast_zero, add_zero]
  | succ n IH =>
    rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]

Iterated Successor as Addition: $\mathrm{succ}^{[n]}(x) = x + n$

Informal description

Let $\alpha$ be a type equipped with a preorder, an addition operation, a distinguished element $1$, and a `SuccAddOrder` structure (where $\mathrm{succ}(x) = x + 1$ for all $x \in \alpha$). Then for any $x \in \alpha$ and any natural number $n$, the $n$-th iterate of the successor function applied to $x$ equals $x + n$, i.e., $\mathrm{succ}^{[n]}(x) = x + n$.

Order.pred_iterate theorem

[AddCommGroupWithOne α] [PredSubOrder α] (x : α) (n : ℕ) : pred^[n] x = x - n

Full source

@[simp]
theorem pred_iterate [AddCommGroupWithOne α] [PredSubOrder α] (x : α) (n : ℕ) :
    predpred^[n] x = x - n := by
  induction n with
  | zero =>
    rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]
  | succ n IH =>
    rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]

Iterated Predecessor as Subtraction: $\mathrm{pred}^{[n]}(x) = x - n$

Informal description

Let $\alpha$ be an additive commutative group with one, equipped with a `PredSubOrder` structure where $\mathrm{pred}(x) = x - 1$ for all $x \in \alpha$. Then for any $x \in \alpha$ and any natural number $n$, the $n$-th iterate of the predecessor function satisfies $\mathrm{pred}^{[n]}(x) = x - n$.

Order.not_isMax_zero theorem

[Zero α] [One α] [ZeroLEOneClass α] [NeZero (1 : α)] : ¬IsMax (0 : α)

Full source

theorem not_isMax_zero [Zero α] [One α] [ZeroLEOneClass α] [NeZero (1 : α)] : ¬ IsMax (0 : α) := by
  rw [not_isMax_iff]
  exact ⟨1, one_pos⟩

Non-Maximality of Zero in Ordered Structures with $0 \leq 1$ and $1 \neq 0$

Informal description

In a type $\alpha$ with elements $0$ and $1$, a relation $\leq$ satisfying $0 \leq 1$, and where $1$ is non-zero, the element $0$ is not maximal.

Order.one_le_iff_pos theorem

[AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero (1 : α)] [SuccAddOrder α] : 1 ≤ x ↔ 0 < x

Full source

theorem one_le_iff_pos [AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero (1 : α)]
    [SuccAddOrder α] : 1 ≤ x ↔ 0 < x := by
  rw [← succ_le_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]

Characterization of Positivity via One: $1 \leq x \leftrightarrow 0 < x$

Informal description

Let $\alpha$ be an additive monoid with one, equipped with a partial order satisfying $0 \leq 1$ and $1 \neq 0$, and where the successor function satisfies $\mathrm{succ}(x) = x + 1$. Then for any $x \in \alpha$, we have $1 \leq x$ if and only if $0 < x$.

Order.covBy_iff_add_one_eq theorem

[Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] : x ⋖ y ↔ x + 1 = y

Full source

theorem covBy_iff_add_one_eq [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] :
    x ⋖ yx ⋖ y ↔ x + 1 = y := by
  rw [← succ_eq_add_one]
  exact succ_eq_iff_covBy.symm

Covering Relation Characterization via Successor: $x \lessdot y \leftrightarrow y = x + 1$

Informal description

Let $\alpha$ be a type equipped with addition, a distinguished element $1$, and a partial order where the successor function satisfies $\mathrm{succ}(x) = x + 1$ for all $x \in \alpha$, and assume $\alpha$ has no maximal elements. Then for any elements $x, y \in \alpha$, we have that $x$ is covered by $y$ (denoted $x \lessdot y$) if and only if $y = x + 1$. In symbols: $$x \lessdot y \leftrightarrow y = x + 1.$$

Order.covBy_iff_sub_one_eq theorem

[Sub α] [One α] [PredSubOrder α] [NoMinOrder α] : x ⋖ y ↔ y - 1 = x

Full source

theorem covBy_iff_sub_one_eq [Sub α] [One α] [PredSubOrder α] [NoMinOrder α] :
    x ⋖ yx ⋖ y ↔ y - 1 = x := by
  rw [← pred_eq_sub_one]
  exact pred_eq_iff_covBy.symm

Covering Relation Characterization via Subtraction: $x \lessdot y \leftrightarrow y - 1 = x$

Informal description

Let $\alpha$ be a type equipped with a subtraction operation, a distinguished element $1$, and a `PredSubOrder` structure where $\mathrm{pred}(x) = x - 1$ for all $x \in \alpha$. If $\alpha$ has no minimal elements, then for any elements $x, y \in \alpha$, we have $x \lessdot y$ (i.e., $y$ covers $x$) if and only if $y - 1 = x$.

Order.IsSuccPrelimit.add_one_lt theorem

[Add α] [One α] [SuccAddOrder α] (hx : IsSuccPrelimit x) (hy : y < x) : y + 1 < x

Full source

theorem IsSuccPrelimit.add_one_lt [Add α] [One α] [SuccAddOrder α]
    (hx : IsSuccPrelimit x) (hy : y < x) : y + 1 < x := by
  rw [← succ_eq_add_one]
  exact hx.succ_lt hy

Successor Pre-Limit Implies $y + 1 < x$ for $y < x$

Informal description

Let $\alpha$ be a type equipped with a partial order, addition, and a distinguished element $1$, such that the successor function satisfies $\mathrm{succ}(x) = x + 1$ for all $x \in \alpha$. If $x$ is a successor pre-limit (i.e., there is no element covered by $x$) and $y < x$, then $y + 1 < x$.

Order.IsPredPrelimit.lt_sub_one theorem

[Sub α] [One α] [PredSubOrder α] (hx : IsPredPrelimit x) (hy : x < y) : x < y - 1

Full source

theorem IsPredPrelimit.lt_sub_one [Sub α] [One α] [PredSubOrder α]
    (hx : IsPredPrelimit x) (hy : x < y) : x < y - 1 := by
  rw [← pred_eq_sub_one]
  exact hx.lt_pred hy

Predecessor Pre-Limit Implies $x < y - 1$ for $x < y$

Informal description

Let $\alpha$ be a type equipped with a partial order, subtraction, and a distinguished element $1$, such that the predecessor function satisfies $\mathrm{pred}(x) = x - 1$ for all $x \in \alpha$. If $x$ is a predecessor pre-limit (i.e., there is no element covering $x$) and $x < y$, then $x < y - 1$.

Order.IsSuccLimit.add_one_lt theorem

[Add α] [One α] [SuccAddOrder α] (hx : IsSuccLimit x) (hy : y < x) : y + 1 < x

Full source

theorem IsSuccLimit.add_one_lt [Add α] [One α] [SuccAddOrder α]
    (hx : IsSuccLimit x) (hy : y < x) : y + 1 < x :=
  hx.isSuccPrelimit.add_one_lt hy

Successor Limit Implies $y + 1 < x$ for $y < x$

Informal description

Let $\alpha$ be a type equipped with a partial order, addition, and a distinguished element $1$, such that the successor function satisfies $\mathrm{succ}(x) = x + 1$ for all $x \in \alpha$. If $x$ is a successor limit (i.e., $x$ is not minimal and does not cover any other element) and $y < x$, then $y + 1 < x$.

Order.IsPredLimit.lt_sub_one theorem

[Sub α] [One α] [PredSubOrder α] (hx : IsPredLimit x) (hy : x < y) : x < y - 1

Full source

theorem IsPredLimit.lt_sub_one [Sub α] [One α] [PredSubOrder α]
    (hx : IsPredLimit x) (hy : x < y) : x < y - 1 :=
  hx.isPredPrelimit.lt_sub_one hy

Predecessor Limit Implies $x < y - 1$ for $x < y$

Informal description

Let $\alpha$ be a type equipped with a partial order, subtraction, and a distinguished element $1$, such that the predecessor function satisfies $\mathrm{pred}(x) = x - 1$ for all $x \in \alpha$. If $x$ is a predecessor limit (i.e., $x$ is not maximal and does not cover any other element) and $x < y$, then $x < y - 1$.

Order.IsSuccPrelimit.add_natCast_lt theorem

[AddMonoidWithOne α] [SuccAddOrder α] (hx : IsSuccPrelimit x) (hy : y < x) : ∀ n : ℕ, y + n < x

Full source

theorem IsSuccPrelimit.add_natCast_lt [AddMonoidWithOne α] [SuccAddOrder α]
    (hx : IsSuccPrelimit x) (hy : y < x) : ∀ n : ℕ, y + n < x
  | 0 => by simpa
  | n + 1 => by
    rw [Nat.cast_add_one, ← add_assoc]
    exact hx.add_one_lt (hx.add_natCast_lt hy n)

Successor Pre-Limit Implies $y + n < x$ for All $n \in \mathbb{N}$ When $y < x$

Informal description

Let $\alpha$ be a type equipped with a partial order, addition, a distinguished element $1$, and a successor function satisfying $\mathrm{succ}(x) = x + 1$ for all $x \in \alpha$. If $x$ is a successor pre-limit (i.e., there is no element covered by $x$) and $y < x$, then for any natural number $n$, we have $y + n < x$.

Order.IsPredPrelimit.lt_sub_natCast theorem

[AddCommGroupWithOne α] [PredSubOrder α] (hx : IsPredPrelimit x) (hy : x < y) : ∀ n : ℕ, x < y - n

Full source

theorem IsPredPrelimit.lt_sub_natCast [AddCommGroupWithOne α] [PredSubOrder α]
    (hx : IsPredPrelimit x) (hy : x < y) : ∀ n : ℕ, x < y - n
  | 0 => by simpa
  | n + 1 => by
    rw [Nat.cast_add_one, ← sub_sub]
    exact hx.lt_sub_one (hx.lt_sub_natCast hy n)

Predecessor Pre-Limit Implies $x < y - n$ for All $n \in \mathbb{N}$ When $x < y$

Informal description

Let $\alpha$ be a type equipped with a partial order, addition, subtraction, and a distinguished element $1$, such that the predecessor function satisfies $\mathrm{pred}(x) = x - 1$ for all $x \in \alpha$. If $x$ is a predecessor pre-limit (i.e., there is no element covering $x$) and $x < y$, then for any natural number $n$, we have $x < y - n$.

Order.IsSuccLimit.add_natCast_lt theorem

[AddMonoidWithOne α] [SuccAddOrder α] (hx : IsSuccLimit x) (hy : y < x) : ∀ n : ℕ, y + n < x

Full source

theorem IsSuccLimit.add_natCast_lt [AddMonoidWithOne α] [SuccAddOrder α]
    (hx : IsSuccLimit x) (hy : y < x) : ∀ n : ℕ, y + n < x :=
  hx.isSuccPrelimit.add_natCast_lt hy

Successor Limit Implies $y + n < x$ for All $n \in \mathbb{N}$ When $y < x$

Informal description

Let $\alpha$ be a type equipped with a partial order, addition, a distinguished element $1$, and a successor function satisfying $\mathrm{succ}(x) = x + 1$ for all $x \in \alpha$. If $x$ is a successor limit (i.e., $x$ is not minimal and does not cover any other element) and $y < x$, then for any natural number $n$, we have $y + n < x$.

Order.IsPredLimit.lt_sub_natCast theorem

[AddCommGroupWithOne α] [PredSubOrder α] (hx : IsPredLimit x) (hy : x < y) : ∀ n : ℕ, x < y - n

Full source

theorem IsPredLimit.lt_sub_natCast [AddCommGroupWithOne α] [PredSubOrder α]
    (hx : IsPredLimit x) (hy : x < y) : ∀ n : ℕ, x < y - n :=
  hx.isPredPrelimit.lt_sub_natCast hy

Predecessor Limit Implies $x < y - n$ for All $n \in \mathbb{N}$ When $x < y$

Informal description

Let $\alpha$ be a type equipped with a partial order, addition, subtraction, and a distinguished element $1$, such that the predecessor function satisfies $\mathrm{pred}(x) = x - 1$ for all $x \in \alpha$. If $x$ is a predecessor limit (i.e., $x$ is not maximal and does not cover any other element) and $x < y$, then for any natural number $n$, we have $x < y - n$.

Order.IsSuccLimit.natCast_lt theorem

[AddMonoidWithOne α] [SuccAddOrder α] [CanonicallyOrderedAdd α] (hx : IsSuccLimit x) : ∀ n : ℕ, n < x

Full source

theorem IsSuccLimit.natCast_lt [AddMonoidWithOne α] [SuccAddOrder α] [CanonicallyOrderedAdd α]
    (hx : IsSuccLimit x) : ∀ n : ℕ, n < x := by
  simpa [bot_eq_zero] using hx.add_natCast_lt hx.bot_lt

Natural Numbers Below Successor Limit in Canonically Ordered Monoid

Informal description

Let $\alpha$ be a canonically ordered additive monoid with one, equipped with a successor function satisfying $\mathrm{succ}(x) = x + 1$ for all $x \in \alpha$. If $x$ is a successor limit element (i.e., $x$ is not minimal and does not cover any other element), then for every natural number $n$, we have $n < x$.

Order.not_isSuccLimit_natCast theorem

[AddMonoidWithOne α] [SuccAddOrder α] [CanonicallyOrderedAdd α] (n : ℕ) : ¬IsSuccLimit (n : α)

Full source

theorem not_isSuccLimit_natCast [AddMonoidWithOne α] [SuccAddOrder α] [CanonicallyOrderedAdd α]
    (n : ℕ) : ¬ IsSuccLimit (n : α) :=
  fun h ↦ (h.natCast_lt n).false

Natural Numbers Are Not Successor Limits in Canonically Ordered Monoid

Informal description

Let $\alpha$ be a canonically ordered additive monoid with one, equipped with a successor function satisfying $\mathrm{succ}(x) = x + 1$ for all $x \in \alpha$. For any natural number $n$, the element $n$ (viewed in $\alpha$) is not a successor limit.

Order.succ_eq_zero theorem

 [AddZeroClass α] [CanonicallyOrderedAdd α] [One α] [NoMaxOrder α] [SuccAddOrder α] {a : WithBot α} :
  WithBot.succ a = 0 ↔ a = ⊥

Full source

@[simp]
theorem succ_eq_zero [AddZeroClass α] [CanonicallyOrderedAdd α] [One α] [NoMaxOrder α]
    [SuccAddOrder α] {a : WithBot α} : WithBot.succWithBot.succ a = 0 ↔ a = ⊥ := by
  cases a
  · simp [bot_eq_zero]
  · rename_i a
    simp only [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false]
    by_contra h
    simpa [h] using max_of_succ_le (a := a)

Successor Equals Zero Criterion in $\text{WithBot}(\alpha)$: $\text{succ}(a) = 0 \leftrightarrow a = \bot$

Informal description

Let $\alpha$ be a type equipped with an additive zero class structure, a canonical order, a distinguished element $1$, and no maximal elements. Suppose further that $\alpha$ has a successor function satisfying $\text{succ}(x) = x + 1$ for all $x \in \alpha$. For any element $a$ in $\text{WithBot}(\alpha)$, the successor of $a$ equals $0$ if and only if $a$ is the bottom element $\bot$.

Order.le_of_lt_add_one theorem

(h : x < y + 1) : x ≤ y

Full source

theorem le_of_lt_add_one (h : x < y + 1) : x ≤ y := by
  rw [← succ_eq_add_one] at h
  exact le_of_lt_succ h

Strictly Below Successor Implies Non-Strictly Below: $x < y + 1 \implies x \leq y$

Informal description

For any elements $x$ and $y$ in an ordered type $\alpha$ with addition and a distinguished element $1$, if $x < y + 1$, then $x \leq y$.

Order.lt_add_one_iff_of_not_isMax theorem

(hy : ¬IsMax y) : x < y + 1 ↔ x ≤ y

Full source

theorem lt_add_one_iff_of_not_isMax (hy : ¬ IsMax y) : x < y + 1 ↔ x ≤ y := by
  rw [← succ_eq_add_one, lt_succ_iff_of_not_isMax hy]

Characterization of Strictly Below Successor for Non-Maximal Elements: $x < y + 1 \leftrightarrow x \leq y$

Informal description

For any elements $x$ and $y$ in a preorder $\alpha$ with addition and a distinguished element $1$, if $y$ is not maximal, then $x < y + 1$ if and only if $x \leq y$.

Order.lt_add_one_iff theorem

[NoMaxOrder α] : x < y + 1 ↔ x ≤ y

Full source

theorem lt_add_one_iff [NoMaxOrder α] : x < y + 1 ↔ x ≤ y :=
  lt_add_one_iff_of_not_isMax (not_isMax y)

Characterization of Strictly Below Successor in Orders without Maximal Elements: $x < y + 1 \leftrightarrow x \leq y$

Informal description

In a preorder $\alpha$ with no maximal elements, for any elements $x$ and $y$, the inequality $x < y + 1$ holds if and only if $x \leq y$.

Order.le_of_sub_one_lt theorem

(h : x - 1 < y) : x ≤ y

Full source

theorem le_of_sub_one_lt (h : x - 1 < y) : x ≤ y := by
  rw [← pred_eq_sub_one] at h
  exact le_of_pred_lt h

Implication from Subtraction-Strict Inequality to Non-strict Inequality

Informal description

For any elements $x$ and $y$ in a preorder $\alpha$ equipped with subtraction and a distinguished element $1$, if $x - 1 < y$, then $x \leq y$.

Order.sub_one_lt_iff_of_not_isMin theorem

(hx : ¬IsMin x) : x - 1 < y ↔ x ≤ y

Full source

theorem sub_one_lt_iff_of_not_isMin (hx : ¬ IsMin x) : x - 1 < y ↔ x ≤ y := by
  rw [← pred_eq_sub_one, pred_lt_iff_of_not_isMin hx]

Subtraction-Strict Inequality Equivalence for Non-Minimal Elements

Informal description

For any element $x$ in a preorder $\alpha$ equipped with subtraction and a distinguished element $1$, if $x$ is not minimal, then $x - 1 < y$ if and only if $x \leq y$.

Order.sub_one_lt_iff theorem

[NoMinOrder α] : x - 1 < y ↔ x ≤ y

Full source

theorem sub_one_lt_iff [NoMinOrder α] : x - 1 < y ↔ x ≤ y :=
  sub_one_lt_iff_of_not_isMin (not_isMin x)

Subtraction-Strict Inequality Equivalence in Orders Without Minimal Elements: $x - 1 < y \leftrightarrow x \leq y$

Informal description

In a preorder $\alpha$ with no minimal elements and equipped with subtraction and a distinguished element $1$, for any elements $x, y \in \alpha$, the inequality $x - 1 < y$ holds if and only if $x \leq y$.

Order.lt_one_iff_nonpos theorem

[AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero (1 : α)] [SuccAddOrder α] : x < 1 ↔ x ≤ 0

Full source

theorem lt_one_iff_nonpos [AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero (1 : α)]
    [SuccAddOrder α] : x < 1 ↔ x ≤ 0 := by
  rw [← lt_succ_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]

Characterization of Elements Less Than One: $x < 1 \leftrightarrow x \leq 0$ in Ordered Additive Monoids with Successor

Informal description

Let $\alpha$ be a type equipped with an additive monoid structure with a distinguished element $1$, a relation $\leq$ satisfying $0 \leq 1$, and a successor function such that $\mathrm{succ}(x) = x + 1$ for all $x \in \alpha$. If $1 \neq 0$ in $\alpha$, then for any $x \in \alpha$, we have $x < 1$ if and only if $x \leq 0$.

monotoneOn_of_le_add_one theorem

(hs : s.OrdConnected) : (∀ a, ¬IsMax a → a ∈ s → a + 1 ∈ s → f a ≤ f (a + 1)) → MonotoneOn f s

Full source

lemma monotoneOn_of_le_add_one (hs : s.OrdConnected) :
    (∀ a, ¬ IsMax a → a ∈ s → a + 1 ∈ s → f a ≤ f (a + 1)) → MonotoneOn f s := by
  simpa [Order.succ_eq_add_one] using monotoneOn_of_le_succ hs (f := f)

Monotonicity Criterion via Addition by One on Order-Connected Sets: $f(a) \leq f(a+1) \Rightarrow f$ monotone on $s$

Informal description

Let $s$ be an order-connected subset of a preorder $\alpha$ equipped with addition and a distinguished element $1$ such that $\mathrm{succ}(x) = x + 1$ for all $x \in \alpha$. If for every non-maximal element $a \in s$ such that $a + 1 \in s$, the inequality $f(a) \leq f(a + 1)$ holds, then the function $f$ is monotone on $s$.

antitoneOn_of_add_one_le theorem

(hs : s.OrdConnected) : (∀ a, ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) ≤ f a) → AntitoneOn f s

Full source

lemma antitoneOn_of_add_one_le (hs : s.OrdConnected) :
    (∀ a, ¬ IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) ≤ f a) → AntitoneOn f s := by
  simpa [Order.succ_eq_add_one] using antitoneOn_of_succ_le hs (f := f)

Antitonicity Criterion via Addition by One on Order-Connected Sets: $f(a+1) \leq f(a) \Rightarrow f$ antitone on $s$

Informal description

Let $s$ be an order-connected subset of a preorder $\alpha$ equipped with addition and a distinguished element $1$ (where $\mathrm{succ}(x) = x + 1$). If for every non-maximal element $a \in s$ such that $a + 1 \in s$, the inequality $f(a + 1) \leq f(a)$ holds, then the function $f$ is antitone on $s$.

strictMonoOn_of_lt_add_one theorem

(hs : s.OrdConnected) : (∀ a, ¬IsMax a → a ∈ s → a + 1 ∈ s → f a < f (a + 1)) → StrictMonoOn f s

Full source

lemma strictMonoOn_of_lt_add_one (hs : s.OrdConnected) :
    (∀ a, ¬ IsMax a → a ∈ s → a + 1 ∈ s → f a < f (a + 1)) → StrictMonoOn f s := by
  simpa [Order.succ_eq_add_one] using strictMonoOn_of_lt_succ hs (f := f)

Strict Monotonicity Criterion via Successor-Addition on Order-Connected Sets

Informal description

Let $s$ be an order-connected subset of a preorder $\alpha$ equipped with addition and a distinguished element $1$ (where $\mathrm{succ}(x) = x + 1$). If for every non-maximal element $a \in s$ such that $a + 1 \in s$, we have $f(a) < f(a + 1)$, then $f$ is strictly monotone on $s$.

strictAntiOn_of_add_one_lt theorem

(hs : s.OrdConnected) : (∀ a, ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) < f a) → StrictAntiOn f s

Full source

lemma strictAntiOn_of_add_one_lt (hs : s.OrdConnected) :
    (∀ a, ¬ IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) < f a) → StrictAntiOn f s := by
  simpa [Order.succ_eq_add_one] using strictAntiOn_of_succ_lt hs (f := f)

Strict Antitonicity Criterion via Addition by One on Order-Connected Sets

Informal description

Let $s$ be an order-connected subset of a preorder $\alpha$ equipped with addition and a distinguished element $1$ (where $\mathrm{succ}(x) = x + 1$). If for every non-maximal element $a \in s$ such that $a + 1 \in s$, we have $f(a + 1) < f(a)$, then $f$ is strictly antitone on $s$.

monotone_of_le_add_one theorem

: (∀ a, ¬IsMax a → f a ≤ f (a + 1)) → Monotone f

Full source

lemma monotone_of_le_add_one : (∀ a, ¬ IsMax a → f a ≤ f (a + 1)) → Monotone f := by
  simpa [Order.succ_eq_add_one] using monotone_of_le_succ (f := f)

Monotonicity Criterion via Successor-Addition: $f(a) \leq f(a+1)$ implies Monotonicity

Informal description

Let $\alpha$ be a preorder equipped with addition and a distinguished element $1$ such that $\mathrm{succ}(x) = x + 1$. If a function $f : \alpha \to \beta$ (where $\beta$ is a preorder) satisfies $f(a) \leq f(a + 1)$ for every non-maximal element $a \in \alpha$, then $f$ is monotone.

antitone_of_add_one_le theorem

: (∀ a, ¬IsMax a → f (a + 1) ≤ f a) → Antitone f

Full source

lemma antitone_of_add_one_le : (∀ a, ¬ IsMax a → f (a + 1) ≤ f a) → Antitone f := by
  simpa [Order.succ_eq_add_one] using antitone_of_succ_le (f := f)

Antitonicity via Successor-Addition: $f(a+1) \leq f(a)$ implies Antitonicity

Informal description

Let $\alpha$ be a preorder equipped with addition and a distinguished element $1$ such that $\mathrm{succ}(x) = x + 1$. If a function $f : \alpha \to \beta$ (where $\beta$ is a preorder) satisfies $f(a + 1) \leq f(a)$ for every non-maximal element $a \in \alpha$, then $f$ is antitone.

strictMono_of_lt_add_one theorem

: (∀ a, ¬IsMax a → f a < f (a + 1)) → StrictMono f

Full source

lemma strictMono_of_lt_add_one : (∀ a, ¬ IsMax a → f a < f (a + 1)) → StrictMono f := by
  simpa [Order.succ_eq_add_one] using strictMono_of_lt_succ (f := f)

Strict Monotonicity via $f(a) < f(a + 1)$ Condition

Informal description

Let $f$ be a function on a preorder $\alpha$ equipped with addition and a distinguished element $1$. If for every non-maximal element $a \in \alpha$, we have $f(a) < f(a + 1)$, then $f$ is strictly monotone.

strictAnti_of_add_one_lt theorem

: (∀ a, ¬IsMax a → f (a + 1) < f a) → StrictAnti f

Full source

lemma strictAnti_of_add_one_lt : (∀ a, ¬ IsMax a → f (a + 1) < f a) → StrictAnti f := by
  simpa [Order.succ_eq_add_one] using strictAnti_of_succ_lt (f := f)

Strict Antitonicity via $f(a + 1) < f(a)$ Condition

Informal description

Let $f$ be a function defined on a preorder $\alpha$ equipped with addition and a distinguished element $1$. If for every non-maximal element $a \in \alpha$, the value of $f$ at $a + 1$ is strictly less than the value at $a$ (i.e., $f(a + 1) < f(a)$), then $f$ is strictly antitone on $\alpha$.

monotoneOn_of_sub_one_le theorem

(hs : s.OrdConnected) : (∀ a, ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) ≤ f a) → MonotoneOn f s

Full source

lemma monotoneOn_of_sub_one_le (hs : s.OrdConnected) :
    (∀ a, ¬ IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) ≤ f a) → MonotoneOn f s := by
  simpa [Order.pred_eq_sub_one] using monotoneOn_of_pred_le hs (f := f)

Monotonicity via $f(a - 1) \leq f(a)$ on Order-Connected Sets

Informal description

Let $s$ be an order-connected subset of a preorder $\alpha$ equipped with subtraction and a distinguished element $1$. If for every non-minimal element $a \in s$ such that $a - 1 \in s$, we have $f(a - 1) \leq f(a)$, then the function $f$ is monotone on $s$.

antitoneOn_of_le_sub_one theorem

(hs : s.OrdConnected) : (∀ a, ¬IsMin a → a ∈ s → a - 1 ∈ s → f a ≤ f (a - 1)) → AntitoneOn f s

Full source

lemma antitoneOn_of_le_sub_one (hs : s.OrdConnected) :
    (∀ a, ¬ IsMin a → a ∈ s → a - 1 ∈ s → f a ≤ f (a - 1)) → AntitoneOn f s := by
  simpa [Order.pred_eq_sub_one] using antitoneOn_of_le_pred hs (f := f)

Antitonicity Criterion via $f(a) \leq f(a - 1)$ on Order-Connected Sets

Informal description

Let $s$ be an order-connected subset of a preorder $\alpha$ equipped with subtraction and a distinguished element $1$. If for every non-minimal element $a \in s$ such that $a - 1 \in s$, the function $f$ satisfies $f(a) \leq f(a - 1)$, then $f$ is antitone on $s$.

strictMonoOn_of_sub_one_lt theorem

(hs : s.OrdConnected) : (∀ a, ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) < f a) → StrictMonoOn f s

Full source

lemma strictMonoOn_of_sub_one_lt (hs : s.OrdConnected) :
    (∀ a, ¬ IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) < f a) → StrictMonoOn f s := by
  simpa [Order.pred_eq_sub_one] using strictMonoOn_of_pred_lt hs (f := f)

Strict Monotonicity Criterion via Subtraction by One on Order Connected Sets

Informal description

Let $s$ be an order connected subset of a preorder $\alpha$ equipped with subtraction and a distinguished element $1$. If for every non-minimal element $a \in s$ such that $a - 1 \in s$, the function $f$ satisfies $f(a - 1) < f(a)$, then $f$ is strictly monotone on $s$.

strictAntiOn_of_lt_sub_one theorem

(hs : s.OrdConnected) : (∀ a, ¬IsMin a → a ∈ s → a - 1 ∈ s → f a < f (a - 1)) → StrictAntiOn f s

Full source

lemma strictAntiOn_of_lt_sub_one (hs : s.OrdConnected) :
    (∀ a, ¬ IsMin a → a ∈ s → a - 1 ∈ s → f a < f (a - 1)) → StrictAntiOn f s := by
  simpa [Order.pred_eq_sub_one] using strictAntiOn_of_lt_pred hs (f := f)

Strict Antitonicity Criterion via Subtraction by One on Order Connected Sets

Informal description

Let $s$ be an order connected subset of a preorder $\alpha$ equipped with subtraction and a distinguished element $1$. If for every non-minimal element $a \in s$ such that $a - 1 \in s$, the function $f : \alpha \to \beta$ satisfies $f(a) < f(a - 1)$, then $f$ is strictly antitone on $s$.

monotone_of_sub_one_le theorem

: (∀ a, ¬IsMin a → f (a - 1) ≤ f a) → Monotone f

Full source

lemma monotone_of_sub_one_le : (∀ a, ¬ IsMin a → f (a - 1) ≤ f a) → Monotone f := by
  simpa [Order.pred_eq_sub_one] using monotone_of_pred_le (f := f)

Monotonicity Criterion via $f(a - 1) \leq f(a)$

Informal description

Let $\alpha$ be a preorder equipped with subtraction and a distinguished element $1$. If a function $f : \alpha \to \beta$ satisfies $f(a - 1) \leq f(a)$ for every non-minimal element $a \in \alpha$, then $f$ is monotone.

antitone_of_le_sub_one theorem

: (∀ a, ¬IsMin a → f a ≤ f (a - 1)) → Antitone f

Full source

lemma antitone_of_le_sub_one : (∀ a, ¬ IsMin a → f a ≤ f (a - 1)) → Antitone f := by
  simpa [Order.pred_eq_sub_one] using antitone_of_le_pred (f := f)

Antitonicity Criterion via $f(a) \leq f(a - 1)$

Informal description

Let $\alpha$ be a preorder equipped with subtraction and a distinguished element $1$, and let $f : \alpha \to \beta$ be a function where $\beta$ is also a preorder. If for every non-minimal element $a \in \alpha$, we have $f(a) \leq f(a - 1)$, then $f$ is antitone.

strictMono_of_sub_one_lt theorem

: (∀ a, ¬IsMin a → f (a - 1) < f a) → StrictMono f

Full source

lemma strictMono_of_sub_one_lt : (∀ a, ¬ IsMin a → f (a - 1) < f a) → StrictMono f := by
  simpa [Order.pred_eq_sub_one] using strictMono_of_pred_lt (f := f)

Strict Monotonicity via Subtraction by One

Informal description

Let $\alpha$ be a type with a preorder, subtraction, and a distinguished element $1$, and let $f : \alpha \to \beta$ be a function where $\beta$ is also a preorder. If for every non-minimal element $a \in \alpha$, we have $f(a - 1) < f(a)$, then $f$ is strictly monotone.

strictAnti_of_lt_sub_one theorem

: (∀ a, ¬IsMin a → f a < f (a - 1)) → StrictAnti f

Full source

lemma strictAnti_of_lt_sub_one : (∀ a, ¬ IsMin a → f a < f (a - 1)) → StrictAnti f := by
  simpa [Order.pred_eq_sub_one] using strictAnti_of_lt_pred (f := f)

Strict Antitonicity via $f(a) < f(a - 1)$

Informal description

Let $\alpha$ be a type equipped with a preorder, subtraction, and a distinguished element $1$, and let $f : \alpha \to \beta$ be a function where $\beta$ is also a preorder. If for every non-minimal element $a \in \alpha$, we have $f(a) < f(a - 1)$, then $f$ is strictly antitone.

Todo