Successors and predecessors of integers

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

@[reducible, inline]

instance Int.instSuccOrder : SuccOrder ℤ

Equations

• Int.instSuccOrder = { succ := Int.succ, le_succ := Int.instSuccOrder.proof_2, max_of_succ_le := @Int.instSuccOrder.proof_3, succ_le_of_lt := @Int.instSuccOrder.proof_4 }

instance Int.instSuccAddOrder : SuccAddOrder ℤ

Equations

• Int.instSuccAddOrder = SuccAddOrder.mk Int.instSuccAddOrder.proof_1

@[reducible, inline]

instance Int.instPredOrder : PredOrder ℤ

Equations

• Int.instPredOrder = { pred := Int.pred, pred_le := Int.instPredOrder.proof_1, min_of_le_pred := @Int.instPredOrder.proof_2, le_pred_of_lt := ⋯ }

instance Int.instPredSubOrder : PredSubOrder ℤ

Equations

• Int.instPredSubOrder = PredSubOrder.mk Int.instPredSubOrder.proof_1

@[simp]

theorem Int.succ_eq_succ : Order.succ = succ

@[simp]

theorem Int.pred_eq_pred : Order.pred = pred

@[deprecated Order.one_le_iff_pos (since := "2024-09-04")]

theorem Int.pos_iff_one_le {a : ℤ} : 0 < a ↔ 1 ≤ a

@[deprecated Order.succ_iterate (since := "2024-09-04")]

theorem Int.succ_iterate (a : ℤ) (n : ℕ) : succ^[n] a = a + ↑n

@[deprecated Order.pred_iterate (since := "2024-09-04")]

theorem Int.pred_iterate (a : ℤ) (n : ℕ) : pred^[n] a = a - ↑n

instance Int.instIsSuccArchimedean : IsSuccArchimedean ℤ

instance Int.instIsPredArchimedean : IsPredArchimedean ℤ

Covering relation

@[deprecated Order.covBy_iff_add_one_eq (since := "2024-09-04")]

theorem Int.covBy_iff_succ_eq {m n : ℤ} : m ⋖ n ↔ m + 1 = n

@[deprecated Order.sub_one_covBy (since := "2024-09-04")]

theorem Int.sub_one_covBy (z : ℤ) : z - 1 ⋖ z

@[deprecated Order.covBy_add_one (since := "2024-09-04")]

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 ⋖ b → ↑a ⋖ ↑b

Alias of the reverse direction of Int.natCast_covBy.