Mathlib.Order.Nat

Module docstring

{"# 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). ","### Miscellaneous lemmas "}

Nat.instOrderBot instance

: OrderBot ℕ

Full source

instance instOrderBot : OrderBot ℕ where
  bot := 0
  bot_le := zero_le

Natural Numbers as an Order with Bottom Element 0

Informal description

The natural numbers $\mathbb{N}$ form an order with a bottom element $0$.

Nat.instNoMaxOrder instance

: NoMaxOrder ℕ

Full source

instance instNoMaxOrder : NoMaxOrder ℕ where
  exists_gt n := ⟨n + 1, n.lt_succ_self⟩

No Maximal Element in the Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form an order without maximal elements, meaning that for any natural number $n$, there exists another natural number $m$ such that $n < m$.

Nat.bot_eq_zero theorem

: ⊥ = 0

Full source

@[simp high] protected lemma bot_eq_zero : ⊥ = 0 := rfl

Bottom Element of Natural Numbers is Zero

Informal description

The bottom element of the natural numbers is equal to $0$, i.e., $\bot = 0$.

Nat.isLeast_find theorem

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

Full source

/-- `Nat.find` is the minimum natural number satisfying a predicate `p`. -/
lemma isLeast_find {p : ℕ → Prop} [DecidablePred p] (hp : ∃ n, p n) :
    IsLeast {n | p n} (Nat.find hp) :=
  ⟨Nat.find_spec hp, fun _ ↦ Nat.find_min' hp⟩

Minimal Satisfying Number is Least Element of Predicate Set

Informal description

For any decidable predicate $p$ on natural numbers, if there exists a natural number satisfying $p$, then the minimal natural number satisfying $p$ (denoted by $\text{Nat.find}\, hp$) is the least element of the set $\{n \mid p(n)\}$.

Set.Nonempty.isLeast_natFind theorem

{s : Set ℕ} [DecidablePred (· ∈ s)] (hs : s.Nonempty) : IsLeast s (Nat.find hs)

Full source

/-- `Nat.find` is the minimum element of a nonempty set of natural numbers. -/
lemma Set.Nonempty.isLeast_natFind {s : Set ℕ} [DecidablePred (· ∈ s)] (hs : s.Nonempty) :
    IsLeast s (Nat.find hs) :=
  Nat.isLeast_find hs

Minimal Element of Nonempty Set of Natural Numbers is Least

Informal description

For any nonempty set $s$ of natural numbers with a decidable membership predicate, the minimal natural number in $s$ (denoted by $\text{Nat.find}\, hs$) is the least element of $s$.