The natural numbers form a linear order

This file contains the linear order instance on the natural numbers.

See note [foundational algebra order theory].

TODO

Move the LinearOrder ℕ instance here (https://github.com/leanprover-community/mathlib4/pull/13092).

@[implicit_reducible]

instance Nat.instOrderBot : OrderBot ℕ

Equations

• Nat.instOrderBot = { bot := 0, bot_le := Nat.zero_le }

instance Nat.instNoMaxOrder : NoMaxOrder ℕ

Miscellaneous lemmas

@[simp]

theorem Nat.bot_eq_zero : ⊥ = 0

theorem Nat.isLeast_find {p : ℕ → Prop} [DecidablePred p] (hp : ∃ (n : ℕ), p n) : IsLeast {n : ℕ | p n} (Nat.find hp)

Nat.find is the minimum natural number satisfying a predicate p.

theorem Set.Nonempty.isLeast_natFind {s : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ s] (hs : s.Nonempty) : IsLeast s (Nat.find hs)

Nat.find is the minimum element of a nonempty set of natural numbers.