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.
Instances For
    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
    Instances For
      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_of_le {p q : Prop} [DecidablePred p] [DecidablePred q] {x : } (hx : q x) (hpq : ∀ (n : ), n xq np n) :

      If a predicate q holds at some x and implies p up to that x, then the earliest xq such that q xq is at least the smallest xp where p xp. The stronger version of Nat.find_mono, since this one needs implication only up to Nat.find _ while the other requires q implying p everywhere.

      theorem Nat.find_mono {p q : Prop} [DecidablePred p] [DecidablePred q] (h : ∀ (n : ), q np n) {hp : (n : ), p n} {hq : (n : ), q n} :

      A weak version of Nat.find_mono_of_le, requiring q implies p everywhere.

      theorem Nat.find_congr {p q : Prop} [DecidablePred p] [DecidablePred q] {x : } (hx : p x) (hpq : ∀ (n : ), n x → (p n q n)) :

      If a predicate p holds at some x and agrees with q up to that x, then their Nat.find agree. The stronger version of Nat.find_congr', since this one needs agreement only up to Nat.find _ while the other requires p = q. Usage of this lemma will likely be via obtain ⟨x, hx⟩ := hp; apply Nat.find_congr hx to unify q, or provide it explicitly with rw [Nat.find_congr (q := q) hx].

      theorem Nat.find_congr' {p q : Prop} [DecidablePred p] [DecidablePred q] {hp : (n : ), p n} {hq : (n : ), q n} (hpq : ∀ {n : }, p n q n) :

      A weak version of Nat.find_congr, requiring p = q everywhere.

      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
      Instances For
        @[simp]
        theorem Nat.findGreatest_succ {P : Prop} [DecidablePred P] (n : ) :
        findGreatest P (n + 1) = if P (n + 1) then n + 1 else findGreatest P n
        @[simp]
        theorem Nat.findGreatest_eq {P : Prop} [DecidablePred P] {n : } :
        P nfindGreatest 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] :
        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] :
        findGreatest P k = 0 ∀ ⦃n : ⦄, 0 < nn k¬P n
        @[simp]
        theorem Nat.findGreatest_pos {k : } {P : Prop} [DecidablePred P] :
        0 < 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) :
        P (findGreatest P n)
        theorem Nat.le_findGreatest {m : } {P : Prop} [DecidablePred P] {n : } (hmb : m n) (hm : P m) :
        theorem Nat.findGreatest_mono_right (P : Prop) [DecidablePred P] {m n : } (hmn : m n) :
        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 : findGreatest P n < k) (hkb : k n) :
        ¬P k
        theorem Nat.findGreatest_of_ne_zero {m : } {P : Prop} [DecidablePred P] {n : } (h : findGreatest P n = m) (h0 : m 0) :
        P m