Documentation

Mathlib.Data.Nat.SuccPred

Successors and predecessors of naturals #

In this file, we show that ℕ is both an archimedean succOrder and an archimedean predOrder.

@[reducible, inline]

instance Nat.instSuccOrder :

Equations

Nat.instSuccOrder = SuccOrder.ofSuccLeIff Nat.succ ⋯

instance Nat.instSuccAddOrder :

SuccAddOrder ℕ

Equations

Nat.instSuccAddOrder = { toSuccOrder := Nat.instSuccOrder, succ_eq_add_one := Nat.instSuccAddOrder._proof_1 }

@[reducible, inline]

instance Nat.instPredOrder :

Equations

Nat.instPredOrder = { pred := Nat.pred, pred_le := Nat.pred_le, min_of_le_pred := @Nat.instPredOrder._proof_1, le_pred_of_lt := @Nat.instPredOrder._proof_2 }

instance Nat.instPredSubOrder :

PredSubOrder ℕ

Equations

Nat.instPredSubOrder = { toPredOrder := Nat.instPredOrder, pred_eq_sub_one := Nat.instPredSubOrder._proof_1 }

@[simp]

theorem Nat.succ_eq_succ :

Order.succ = succ

@[simp]

theorem Nat.pred_eq_pred :

Order.pred = pred

theorem Nat.succ_iterate (a n : ℕ) :

succ ^[n] a = a + n

theorem Nat.pred_iterate (a n : ℕ) :

pred ^[n] a = a - n

theorem Nat.le_succ_iff_eq_or_le {m n : ℕ} :

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

instance Nat.instIsSuccArchimedean :

IsSuccArchimedean ℕ

instance Nat.instIsPredArchimedean :

IsPredArchimedean ℕ

theorem Nat.forall_ne_zero_iff (P : ℕ → Prop) :

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

@[simp]

theorem Fin.coe_covBy_iff {n : ℕ} {a b : Fin n} :

↑a ⋖ ↑b ↔ a ⋖ b

theorem CovBy.coe_fin {n : ℕ} {a b : Fin n} :

a ⋖ b → ↑a ⋖ ↑b

Alias of the reverse direction of Fin.coe_covBy_iff.

@[simp]

theorem withBotSucc_zero :

WithBot.succ 0 = 1

@[simp]

theorem withBotSucc_one :

WithBot.succ 1 = 2