Mathlib.Data.Nat.SuccPred

Nat.instSuccOrder abbrev

: SuccOrder ℕ

Full source

@[instance] abbrev instSuccOrder : SuccOrder ℕ :=
  SuccOrder.ofSuccLeIff succ Nat.succ_le

Successor Order Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form a successor order, where for each $n \in \mathbb{N}$, the successor function $\mathrm{succ}(n) = n + 1$ is the least element greater than $n$ in the usual order.

Nat.instSuccAddOrder instance

: SuccAddOrder ℕ

Full source

instance instSuccAddOrder : SuccAddOrder ℕ := ⟨fun _ => rfl⟩

Successor-Addition Order Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form a successor-addition order, where for each $n \in \mathbb{N}$, the successor function $\mathrm{succ}(n) = n + 1$ is the least element greater than $n$ in the usual order, and addition preserves the order structure.

Nat.instPredOrder abbrev

: PredOrder ℕ

Full source

@[instance] abbrev instPredOrder : PredOrder ℕ where
  pred := pred
  pred_le := pred_le
  min_of_le_pred {a} ha := by
    cases a
    · exact isMin_bot
    · exact (not_succ_le_self _ ha).elim
  le_pred_of_lt {a} {b} h := by
    cases b
    · exact (a.not_lt_zero h).elim
    · exact le_of_succ_le_succ h

Predecessor Order Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form a predecessor order, where each non-minimal element has a greatest predecessor, and minimal elements satisfy $\mathrm{pred}~a = a$.

Nat.instPredSubOrder instance

: PredSubOrder ℕ

Full source

instance instPredSubOrder : PredSubOrder ℕ := ⟨fun _ => rfl⟩

Predecessor-Subtraction Order Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form a predecessor-subtraction order, where each non-minimal element has a greatest predecessor, and minimal elements satisfy $\mathrm{pred}~a = a$.

Nat.succ_eq_succ theorem

: Order.succ = succ

Full source

@[simp]
theorem succ_eq_succ : Order.succ = succ :=
  rfl

Successor Function Identity on Natural Numbers: $\mathrm{succ}(n) = n + 1$

Informal description

The successor function `Order.succ` on natural numbers is equal to the standard successor function `succ`, which satisfies $\mathrm{succ}(n) = n + 1$ for all $n \in \mathbb{N}$.

Nat.pred_eq_pred theorem

: Order.pred = pred

Full source

@[simp]
theorem pred_eq_pred : Order.pred = pred :=
  rfl

Predecessor Function Identity on Natural Numbers

Informal description

The predecessor function `Order.pred` on natural numbers is equal to the standard predecessor function `pred`, which satisfies $\mathrm{pred}(n) = n - 1$ for $n > 0$ and $\mathrm{pred}(0) = 0$.

Nat.succ_iterate theorem

(a : ℕ) : ∀ n, succ^[n] a = a + n

Full source

protected theorem succ_iterate (a : ℕ) : ∀ n, succsucc^[n] a = a + n :=
  Order.succ_iterate a

Iterated Successor Equals Addition: $\mathrm{succ}^n(a) = a + n$

Informal description

For any natural number $a$ and any natural number $n$, the $n$-th iterate of the successor function applied to $a$ equals $a + n$, i.e., $\mathrm{succ}^n(a) = a + n$.

Nat.pred_iterate theorem

(a : ℕ) : ∀ n, pred^[n] a = a - n

Full source

protected theorem pred_iterate (a : ℕ) : ∀ n, predpred^[n] a = a - n
  | 0 => rfl
  | n + 1 => by
    rw [Function.iterate_succ', sub_succ]
    exact congr_arg _ (Nat.pred_iterate a n)

Iterated Predecessor Equals Subtraction: $\mathrm{pred}^n(a) = a - n$

Informal description

For any natural number $a$ and any natural number $n$, the $n$-th iterate of the predecessor function applied to $a$ equals $a - n$, i.e., $\mathrm{pred}^n(a) = a - n$.

Nat.le_succ_iff_eq_or_le theorem

: m ≤ n.succ ↔ m = n.succ ∨ m ≤ n

Full source

lemma le_succ_iff_eq_or_le : m ≤ n.succ ↔ m = n.succ ∨ m ≤ n := Order.le_succ_iff_eq_or_le

Characterization of Inequality with Successor: $m \leq n+1 \leftrightarrow m = n+1 \lor m \leq n$

Informal description

For any natural numbers $m$ and $n$, the inequality $m \leq n + 1$ holds if and only if either $m = n + 1$ or $m \leq n$.

Nat.instIsSuccArchimedean instance

: IsSuccArchimedean ℕ

Full source

instance : IsSuccArchimedean ℕ :=
  ⟨fun {a} {b} h => ⟨b - a, by rw [succ_eq_succ, Nat.succ_iterate, add_tsub_cancel_of_le h]⟩⟩

Natural Numbers are Successor-Archimedean

Informal description

The natural numbers $\mathbb{N}$ form a successor-archimedean order, meaning that for any two natural numbers $m \leq n$, there exists a natural number $k$ such that $n \leq m + k$.

Nat.instIsPredArchimedean instance

: IsPredArchimedean ℕ

Full source

instance : IsPredArchimedean ℕ :=
  ⟨fun {a} {b} h => ⟨b - a, by rw [pred_eq_pred, Nat.pred_iterate, tsub_tsub_cancel_of_le h]⟩⟩

Natural Numbers are Pred-Archimedean

Informal description

The natural numbers $\mathbb{N}$ form a pred-archimedean order, meaning that for any two natural numbers $a \leq b$, there exists a natural number $n$ such that applying the predecessor function $n$ times to $b$ yields $a$.

Nat.forall_ne_zero_iff theorem

(P : ℕ → Prop) : (∀ i, i ≠ 0 → P i) ↔ (∀ i, P (i + 1))

Full source

lemma forall_ne_zero_iff (P : ℕ → Prop) :
    (∀ i, i ≠ 0 → P i) ↔ (∀ i, P (i + 1)) :=
  SuccOrder.forall_ne_bot_iff P

Equivalence of Predicate Conditions on Nonzero and Successor Natural Numbers

Informal description

For any predicate $P$ on natural numbers, the following are equivalent: 1. $P(i)$ holds for all nonzero natural numbers $i$. 2. $P(i+1)$ holds for all natural numbers $i$.

Fin.coe_covBy_iff theorem

{n : ℕ} {a b : Fin n} : (a : ℕ) ⋖ b ↔ a ⋖ b

Full source

@[simp, norm_cast]
theorem Fin.coe_covBy_iff {n : ℕ} {a b : Fin n} : (a : ℕ) ⋖ b(a : ℕ) ⋖ b ↔ a ⋖ b :=
  and_congr_right' ⟨fun h _c hc => h hc, fun h c ha hb => @h ⟨c, hb.trans b.prop⟩ ha hb⟩

Covering Relation Preservation under Coercion for Finite Types

Informal description

For any natural number $n$ and elements $a, b$ of the finite type $\text{Fin}\,n$, the natural number coercion of $a$ is covered by $b$ (denoted $a \lessdot b$) if and only if $a$ is covered by $b$ in $\text{Fin}\,n$. Here, $x \lessdot y$ means that $x < y$ and there is no $z$ such that $x < z < y$.

withBotSucc_zero theorem

: WithBot.succ 0 = 1

Full source

@[simp]
theorem withBotSucc_zero : WithBot.succ 0 = 1 := rfl

Successor of Zero in `WithBot ℕ` is One

Informal description

The successor of the element $0$ in the type `WithBot ℕ` is $1$, i.e., $\mathrm{succ}(0) = 1$.

withBotSucc_one theorem

: WithBot.succ 1 = 2

Full source

@[simp]
theorem withBotSucc_one : WithBot.succ 1 = 2 := rfl

Successor of One in `WithBot ℕ` is Two

Informal description

The successor of the element $1$ in the type `WithBot ℕ` is $2$, i.e., $\mathrm{succ}(1) = 2$.