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

• One or more equations did not get rendered due to their size.

@[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 := ⋯, le_of_pred_lt := ⋯ }

@[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

instance Int.instIsSuccArchimedean : IsSuccArchimedean ℤ

Equations

• Int.instIsSuccArchimedean = ⋯

instance Int.instIsPredArchimedean : IsPredArchimedean ℤ

Equations

• Int.instIsPredArchimedean = ⋯

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

Alias of the reverse direction of Int.natCast_covBy.

---

Alias of the reverse direction of Int.natCast_covBy.