mathlib3 documentation

data.int.succ_pred

Successors and predecessors of integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance, reducible]

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, reducible]

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.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

@[protected, instance]

def int.is_succ_archimedean :

is_succ_archimedean ℤ

@[protected, instance]

def int.is_pred_archimedean :

is_pred_archimedean ℤ

Covering relation #

@[protected]

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, norm_cast]

theorem nat.cast_int_covby_iff {a b : ℕ} :

↑a ⋖ ↑b ↔ a ⋖ b

theorem covby.cast_int {a b : ℕ} :

a ⋖ b → ↑a ⋖ ↑b

Alias of the reverse direction of nat.cast_int_covby_iff.