# Nat.find and Nat.findGreatest#

### Nat.find#

def Nat.findX {p : } [] (H : ∃ (n : ), p n) :
{ n : // p n ∀ (m : ), m < n¬p m }
Equations
• One or more equations did not get rendered due to their size.
Instances For
def Nat.find {p : } [] (H : ∃ (n : ), p n) :

If p is a (decidable) predicate on and hp : ∃ (n : ℕ), p n is a proof that there exists some natural number satisfying p, then Nat.find hp is the smallest natural number satisfying p. Note that Nat.find is protected, meaning that you can't just write find, even if the Nat namespace is open.

The API for Nat.find is:

Equations
Instances For
theorem Nat.find_spec {p : } [] (H : ∃ (n : ), p n) :
p (Nat.find H)
theorem Nat.find_min {p : } [] (H : ∃ (n : ), p n) {m : } :
m < ¬p m
theorem Nat.find_min' {p : } [] (H : ∃ (n : ), p n) {m : } (h : p m) :
m
theorem Nat.find_eq_iff {m : } {p : } [] (h : ∃ (n : ), p n) :
= m p m ∀ (n : ), n < m¬p n
@[simp]
theorem Nat.find_lt_iff {p : } [] (h : ∃ (n : ), p n) (n : ) :
< n ∃ (m : ), m < n p m
@[simp]
theorem Nat.find_le_iff {p : } [] (h : ∃ (n : ), p n) (n : ) :
n ∃ (m : ), m n p m
@[simp]
theorem Nat.le_find_iff {p : } [] (h : ∃ (n : ), p n) (n : ) :
n ∀ (m : ), m < n¬p m
@[simp]
theorem Nat.lt_find_iff {p : } [] (h : ∃ (n : ), p n) (n : ) :
n < ∀ (m : ), m n¬p m
@[simp]
theorem Nat.find_eq_zero {p : } [] (h : ∃ (n : ), p n) :
= 0 p 0
theorem Nat.find_mono {p : } {q : } [] [] (h : ∀ (n : ), q np n) {hp : ∃ (n : ), p n} {hq : ∃ (n : ), q n} :
theorem Nat.find_le {n : } {p : } [] {h : ∃ (n : ), p n} (hn : p n) :
n
theorem Nat.find_comp_succ {p : } [] (h₁ : ∃ (n : ), p n) (h₂ : ∃ (n : ), p (n + 1)) (h0 : ¬p 0) :
Nat.find h₁ = Nat.find h₂ + 1
theorem Nat.find_pos {p : } [] (h : ∃ (n : ), p n) :
0 < ¬p 0
theorem Nat.find_add {n : } {p : } [] {hₘ : ∃ (m : ), p (m + n)} {hₙ : ∃ (n : ), p n} (hn : n Nat.find hₙ) :
Nat.find hₘ + n = Nat.find hₙ

### Nat.findGreatest#

def Nat.findGreatest (P : ) [] :

Nat.findGreatest P n is the largest i ≤ bound such that P i holds, or 0 if no such i exists

Equations
Instances For
@[simp]
theorem Nat.findGreatest_zero {P : } [] :
= 0
theorem Nat.findGreatest_succ {P : } [] (n : ) :
Nat.findGreatest P (n + 1) = if P (n + 1) then n + 1 else
@[simp]
theorem Nat.findGreatest_eq {P : } [] {n : } :
P n = n
@[simp]
theorem Nat.findGreatest_of_not {P : } [] {n : } (h : ¬P (n + 1)) :
theorem Nat.findGreatest_eq_iff {m : } {k : } {P : } [] :
= m m k (m 0P m) ∀ ⦃n : ⦄, m < nn k¬P n
theorem Nat.findGreatest_eq_zero_iff {k : } {P : } [] :
= 0 ∀ ⦃n : ⦄, 0 < nn k¬P n
@[simp]
theorem Nat.findGreatest_pos {k : } {P : } [] :
0 < ∃ (n : ), 0 < n n k P n
theorem Nat.findGreatest_spec {m : } {P : } [] {n : } (hmb : m n) (hm : P m) :
theorem Nat.findGreatest_le {P : } [] (n : ) :
n
theorem Nat.le_findGreatest {m : } {P : } [] {n : } (hmb : m n) (hm : P m) :
m
theorem Nat.findGreatest_mono_right (P : ) [] {m : } {n : } (hmn : m n) :
theorem Nat.findGreatest_mono_left {P : } {Q : } [] [] (hPQ : ∀ (n : ), P nQ n) (n : ) :
theorem Nat.findGreatest_mono {m : } {P : } {Q : } [] {n : } [] (hPQ : ∀ (n : ), P nQ n) (hmn : m n) :
theorem Nat.findGreatest_is_greatest {k : } {P : } [] {n : } (hk : < k) (hkb : k n) :
¬P k
theorem Nat.findGreatest_of_ne_zero {m : } {P : } [] {n : } (h : = m) (h0 : m 0) :
P m