Successors and predecessors of naturals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we show that ℕ is both an archimedean succ_order and an archimedean pred_order.

source

@[protected, instance, reducible]

def nat.succ_order :

succ_order ℕ

Equations

nat.succ_order = {succ := nat.succ, le_succ := nat.succ_order._proof_1, max_of_succ_le := nat.succ_order._proof_2, succ_le_of_lt := nat.succ_order._proof_3, le_of_lt_succ := nat.succ_order._proof_4}

source

@[protected, instance, reducible]

def nat.pred_order :

pred_order ℕ

Equations

nat.pred_order = {pred := nat.pred, pred_le := nat.pred_le, min_of_le_pred := nat.pred_order._proof_1, le_pred_of_lt := nat.pred_order._proof_2, le_of_pred_lt := nat.pred_order._proof_3}

source

@[simp]

theorem nat.succ_eq_succ :

order.succ = nat.succ

source

@[simp]

theorem nat.pred_eq_pred :

order.pred = nat.pred

source

theorem nat.succ_iterate (a n : ℕ) :

nat.succ ^[n] a = a + n

source

theorem nat.pred_iterate (a n : ℕ) :

nat.pred ^[n] a = a - n

source

@[protected, instance]

def nat.is_succ_archimedean :

is_succ_archimedean ℕ

source

@[protected, instance]

def nat.is_pred_archimedean :

is_pred_archimedean ℕ

Covering relation #

source

@[protected]

theorem nat.covby_iff_succ_eq {m n : ℕ} :

m ⋖ n ↔ m + 1 = n

source

@[simp, norm_cast]

theorem fin.coe_covby_iff {n : ℕ} {a b : fin n} :

↑a ⋖ ↑b ↔ a ⋖ b

source

theorem covby.coe_fin {n : ℕ} {a b : fin n} :

a ⋖ b → ↑a ⋖ ↑b

Alias of the reverse direction of fin.coe_covby_iff.