mathlib documentation

data.int.succ_pred

Successors and predecessors of integers #

In this file, we show that ℤ is both an archimedean succ_order and an archimedean pred_order.

@[protected, instance]

def int.succ_order :

Equations

int.succ_order = {succ := int.succ, le_succ := int.succ_order._proof_1, max_of_succ_le := int.succ_order._proof_2, succ_le_of_lt := int.succ_order._proof_3, le_of_lt_succ := int.succ_order._proof_4}

@[protected, instance]

def int.pred_order :

Equations

int.pred_order = {pred := int.pred, pred_le := int.pred_order._proof_1, min_of_le_pred := int.pred_order._proof_2, le_pred_of_lt := int.pred_order._proof_3, le_of_pred_lt := int.pred_order._proof_4}

@[simp]

theorem int.succ_eq_succ :

order.succ = int.succ

@[simp]

theorem int.pred_eq_pred :

order.pred = int.pred

theorem int.succ_iterate (a : ℤ) (n : ℕ) :

int.succ ^[n] a = a + ↑n

theorem int.pred_iterate (a : ℤ) (n : ℕ) :

int.pred ^[n] a = a - ↑n

@[protected, instance]

def int.is_succ_archimedean :

is_succ_archimedean ℤ

@[protected, instance]

def int.is_pred_archimedean :

is_pred_archimedean ℤ