Documentation

Mathlib.Data.Nat.Find

Nat.find and Nat.findGreatest #

Nat.find #

def Nat.findX {p : Prop} [DecidablePred 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.
def Nat.find {p : Prop} [DecidablePred 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
theorem Nat.find_spec {p : Prop} [DecidablePred p] (H : ∃ (n : ), p n) :
p (Nat.find H)
theorem Nat.find_min {p : Prop} [DecidablePred p] (H : ∃ (n : ), p n) {m : } :
m < Nat.find H¬p m
theorem Nat.find_min' {p : Prop} [DecidablePred p] (H : ∃ (n : ), p n) {m : } (h : p m) :
theorem Nat.find_eq_iff {m : } {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) :
Nat.find h = m p m ∀ (n : ), n < m¬p n
@[simp]
theorem Nat.find_lt_iff {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) (n : ) :
Nat.find h < n ∃ (m : ), m < n p m
@[simp]
theorem Nat.find_le_iff {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) (n : ) :
Nat.find h n ∃ (m : ), m n p m
@[simp]
theorem Nat.le_find_iff {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) (n : ) :
n Nat.find h ∀ (m : ), m < n¬p m
@[simp]
theorem Nat.lt_find_iff {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) (n : ) :
n < Nat.find h ∀ (m : ), m n¬p m
@[simp]
theorem Nat.find_eq_zero {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) :
Nat.find h = 0 p 0
theorem Nat.find_mono {p q : Prop} [DecidablePred p] [DecidablePred q] (h : ∀ (n : ), q np n) {hp : ∃ (n : ), p n} {hq : ∃ (n : ), q n} :
theorem Nat.find_le {n : } {p : Prop} [DecidablePred p] {h : ∃ (n : ), p n} (hn : p n) :
theorem Nat.find_comp_succ {p : Prop} [DecidablePred 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 : Prop} [DecidablePred p] (h : ∃ (n : ), p n) :
0 < Nat.find h ¬p 0
theorem Nat.find_add {n : } {p : Prop} [DecidablePred 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 : Prop) [DecidablePred P] :

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

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