Successors and predecessors of naturals #
In this file, we show that ℕ
is both an archimedean succOrder
and an archimedean predOrder
.
@[reducible]
@[reducible]
Covering relation #
Alias of the reverse direction of Fin.coe_covby_iff
.
Mathlib.Data.Nat.SuccPred
In this file, we show that ℕ
is both an archimedean succOrder
and an archimedean predOrder
.
Alias of the reverse direction of Fin.coe_covby_iff
.