Successors and predecessors of naturals

In this file, we show that ℕ is both an archimedean succOrder and an archimedean predOrder.

@[reducible]

instance Nat.instSuccOrderNatToPreorderToPartialOrderStrictOrderedSemiring : SuccOrder ℕ

Equations

• Nat.instSuccOrderNatToPreorderToPartialOrderStrictOrderedSemiring = SuccOrder.ofSuccLeIff Nat.succ (_ : ∀ {a b : ℕ}, Nat.succ a ≤ b ↔ a < b)

@[reducible]

instance Nat.instPredOrderNatToPreorderToPartialOrderStrictOrderedSemiring : PredOrder ℕ

Equations

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

@[simp]

theorem Nat.succ_eq_succ : Order.succ = Nat.succ

@[simp]

theorem Nat.pred_eq_pred : Order.pred = Nat.pred

theorem Nat.succ_iterate (a : ℕ) (n : ℕ) : Nat.succ^[n] a = a + n

theorem Nat.pred_iterate (a : ℕ) (n : ℕ) : Nat.pred^[n] a = a - n

instance Nat.instIsSuccArchimedeanNatToPreorderToPartialOrderStrictOrderedSemiringInstSuccOrderNatToPreorderToPartialOrderStrictOrderedSemiring : IsSuccArchimedean ℕ

Equations

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

instance Nat.instIsPredArchimedeanNatToPreorderToPartialOrderStrictOrderedSemiringInstPredOrderNatToPreorderToPartialOrderStrictOrderedSemiring : IsPredArchimedean ℕ

Equations

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

theorem Nat.forall_ne_zero_iff (P : ℕ → Prop) : ((i : ℕ) → i ≠ 0 → P i) ↔ (i : ℕ) → P (i + 1)

Covering relation

theorem Nat.covby_iff_succ_eq {m : ℕ} {n : ℕ} : m ⋖ n ↔ m + 1 = n

@[simp]

theorem Fin.coe_covby_iff {n : ℕ} {a : Fin n} {b : Fin n} : ↑a ⋖ ↑b ↔ a ⋖ b

theorem Covby.coe_fin {n : ℕ} {a : Fin n} {b : Fin n} : a ⋖ b → ↑a ⋖ ↑b

Alias of the reverse direction of Fin.coe_covby_iff.