Successors and predecessors of integers

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

ink

instance Int.instSuccOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRing : SuccOrder ℤ

Equations

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

ink

instance Int.instPredOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRing : PredOrder ℤ

Equations

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

ink

@[simp]

theorem Int.succ_eq_succ : Order.succ = Int.succ

ink

@[simp]

theorem Int.pred_eq_pred : Order.pred = Int.pred

ink

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

ink

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

ink

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

ink

instance Int.instIsSuccArchimedeanIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRingInstSuccOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRing : IsSuccArchimedean ℤ

Equations

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

ink

instance Int.instIsPredArchimedeanIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRingInstPredOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRing : IsPredArchimedean ℤ

Equations

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

Covering relation

ink

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

ink

@[simp]

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

ink

@[simp]

theorem Int.covby_add_one (z : ℤ) : z ⋖ z + 1

ink

@[simp]

theorem Nat.cast_int_covby_iff {a : ℕ} {b : ℕ} : ↑a ⋖ ↑b ↔ a ⋖ b

ink

theorem Covby.cast_int {a : ℕ} {b : ℕ} : a ⋖ b → ↑a ⋖ ↑b

Alias of the reverse direction of Nat.cast_int_covby_iff.