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]
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Nat.succ_eq_succ :
Order.succ = Nat.succ
@[simp]
theorem Nat.pred_eq_pred :
Order.pred = Nat.pred
theorem Nat.succ_iterate (a : ) (n : ) :
Nat.succ^[n] a = a + n
theorem Nat.pred_iterate (a : ) (n : ) :
Nat.pred^[n] a = a - n
theorem Nat.forall_ne_zero_iff (P : Prop) :
((i : ) → i 0P i) (i : ) → P (i + 1)

Covering relation #

theorem Nat.covby_iff_succ_eq {m : } {n : } :
m n m + 1 = n
@[simp]
theorem Fin.coe_covby_iff {n : } {a : Fin n} {b : Fin n} :
a b a b
theorem Covby.coe_fin {n : } {a : Fin n} {b : Fin n} :
a ba b

Alias of the reverse direction of Fin.coe_covby_iff.