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.

source
@[reducible, inline]
instance Nat.instSuccOrder :
SuccOrder ℕ
Equations
    source
    instance Nat.instSuccAddOrder :
    SuccAddOrder ℕ
    Equations
      source
      @[reducible, inline]
      instance Nat.instPredOrder :
      PredOrder ℕ
      Equations
        source
        instance Nat.instPredSubOrder :
        PredSubOrder ℕ
        Equations
          source
          @[simp]
          theorem Nat.succ_eq_succ :
          Order.succ = succ
          source
          @[simp]
          theorem Nat.pred_eq_pred :
          Order.pred = pred
          source
          theorem Nat.succ_iterate (a n : ℕ) :
          succ^[n] a = a + n
          source
          theorem Nat.pred_iterate (a n : ℕ) :
          pred^[n] a = a - n
          source
          theorem Nat.le_succ_iff_eq_or_le {m n : ℕ} :
          m ≤ n.succ ↔ m = n.succ ∨ m ≤ n
          source
          instance Nat.instIsSuccArchimedean :
          IsSuccArchimedean ℕ
          source
          instance Nat.instIsPredArchimedean :
          IsPredArchimedean ℕ
          source
          theorem Nat.forall_ne_zero_iff (P : ℕ → Prop) :
          (∀ (i : ℕ), i ≠ 0 → P i) ↔ ∀ (i : ℕ), P (i + 1)
          source
          @[simp]
          theorem Fin.coe_covBy_iff {n : ℕ} {a b : Fin n} :
          ↑a ⋖ ↑b ↔ a ⋖ b
          source
          theorem CovBy.coe_fin {n : ℕ} {a b : Fin n} :
          a ⋖ b → ↑a ⋖ ↑b

          Alias of the reverse direction of Fin.coe_covBy_iff.

          source
          @[simp]
          theorem withBotSucc_zero :
          WithBot.succ 0 = 1
          source
          @[simp]
          theorem withBotSucc_one :
          WithBot.succ 1 = 2