Successors and predecessors of integers

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

@[reducible]

instance Int.instSuccOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingInstLinearOrderedCommRing : SuccOrder ℤ

Equations

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

@[reducible]

instance Int.instPredOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingInstLinearOrderedCommRing : PredOrder ℤ

Equations

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

@[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.instIsSuccArchimedeanIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingInstLinearOrderedCommRingInstSuccOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingInstLinearOrderedCommRing : IsSuccArchimedean ℤ

Equations

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

instance Int.instIsPredArchimedeanIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingInstLinearOrderedCommRingInstPredOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingInstLinearOrderedCommRing : IsPredArchimedean ℤ

Equations

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

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