Documentation

Mathlib.Data.Int.SuccPred

Successors and predecessors of integers #

In this file, we show that is both an archimedean SuccOrder and an archimedean PredOrder.

@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
Equations
@[simp]
theorem Int.succ_eq_succ :
Order.succ = Int.succ
@[simp]
theorem Int.pred_eq_pred :
Order.pred = Int.pred
theorem Int.pos_iff_one_le {a : } :
0 < a 1 a
theorem Int.succ_iterate (a : ) (n : ) :
Int.succ^[n] a = a + n
theorem Int.pred_iterate (a : ) (n : ) :
Int.pred^[n] a = a - n

Covering relation #

theorem Int.covBy_iff_succ_eq {m : } {n : } :
m n m + 1 = n
@[simp]
theorem Int.sub_one_covBy (z : ) :
z - 1 z
@[simp]
theorem Int.covBy_add_one (z : ) :
z z + 1
@[simp]
theorem Int.natCast_covBy {a : } {b : } :
a b a b
theorem CovBy.intCast {a : } {b : } :
a ba b

Alias of the reverse direction of Int.natCast_covBy.

@[deprecated Int.natCast_covBy]
theorem Nat.cast_int_covBy_iff {a : } {b : } :
a b a b

Alias of Int.natCast_covBy.

@[deprecated CovBy.intCast]
theorem CovBy.cast_int {a : } {b : } :
a ba b

Alias of the reverse direction of Int.natCast_covBy.


Alias of the reverse direction of Int.natCast_covBy.