HepLean Documentation

Mathlib.Data.Nat.Find

Nat.find and Nat.findGreatest #

Nat.find #

source
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
    source
    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
      source
      theorem Nat.find_spec {p : ℕ → Prop} [DecidablePred p] (H : ∃ (n : ℕ), p n) :
      p (Nat.find H)
      source
      theorem Nat.find_min {p : ℕ → Prop} [DecidablePred p] (H : ∃ (n : ℕ), p n) {m : ℕ} :
      m < Nat.find H → ¬p m
      source
      theorem Nat.find_min' {p : ℕ → Prop} [DecidablePred p] (H : ∃ (n : ℕ), p n) {m : ℕ} (h : p m) :
      Nat.find H ≤ m
      source
      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
      source
      @[simp]
      theorem Nat.find_lt_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) :
      Nat.find h < n ↔ ∃ (m : ℕ), m < n ∧ p m
      source
      @[simp]
      theorem Nat.find_le_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) :
      Nat.find h ≤ n ↔ ∃ (m : ℕ), m ≤ n ∧ p m
      source
      @[simp]
      theorem Nat.le_find_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) :
      n ≤ Nat.find h ↔ ∀ (m : ℕ), m < n → ¬p m
      source
      @[simp]
      theorem Nat.lt_find_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) :
      n < Nat.find h ↔ ∀ (m : ℕ), m ≤ n → ¬p m
      source
      @[simp]
      theorem Nat.find_eq_zero {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) :
      Nat.find h = 0 ↔ p 0
      source
      theorem Nat.find_mono {p q : ℕ → Prop} [DecidablePred p] [DecidablePred q] (h : ∀ (n : ℕ), q n → p n) {hp : ∃ (n : ℕ), p n} {hq : ∃ (n : ℕ), q n} :
      Nat.find hp ≤ Nat.find hq
      source
      theorem Nat.find_le {n : ℕ} {p : ℕ → Prop} [DecidablePred p] {h : ∃ (n : ℕ), p n} (hn : p n) :
      Nat.find h ≤ n
      source
      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
      source
      theorem Nat.find_pos {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) :
      0 < Nat.find h ↔ ¬p 0
      source
      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 #

      source
      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
        source
        @[simp]
        theorem Nat.findGreatest_zero {P : ℕ → Prop} [DecidablePred P] :
        Nat.findGreatest P 0 = 0
        source
        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
        source
        @[simp]
        theorem Nat.findGreatest_eq {P : ℕ → Prop} [DecidablePred P] {n : ℕ} :
        P n → Nat.findGreatest P n = n
        source
        @[simp]
        theorem Nat.findGreatest_of_not {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (h : ¬P (n + 1)) :
        Nat.findGreatest P (n + 1) = Nat.findGreatest P n
        source
        theorem Nat.findGreatest_eq_iff {m k : ℕ} {P : ℕ → Prop} [DecidablePred P] :
        Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
        source
        theorem Nat.findGreatest_eq_zero_iff {k : ℕ} {P : ℕ → Prop} [DecidablePred P] :
        Nat.findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n
        source
        @[simp]
        theorem Nat.findGreatest_pos {k : ℕ} {P : ℕ → Prop} [DecidablePred P] :
        0 < Nat.findGreatest P k ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n
        source
        theorem Nat.findGreatest_spec {m : ℕ} {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (hmb : m ≤ n) (hm : P m) :
        P (Nat.findGreatest P n)
        source
        theorem Nat.findGreatest_le {P : ℕ → Prop} [DecidablePred P] (n : ℕ) :
        Nat.findGreatest P n ≤ n
        source
        theorem Nat.le_findGreatest {m : ℕ} {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (hmb : m ≤ n) (hm : P m) :
        m ≤ Nat.findGreatest P n
        source
        theorem Nat.findGreatest_mono_right (P : ℕ → Prop) [DecidablePred P] {m n : ℕ} (hmn : m ≤ n) :
        Nat.findGreatest P m ≤ Nat.findGreatest P n
        source
        theorem Nat.findGreatest_mono_left {P Q : ℕ → Prop} [DecidablePred P] [DecidablePred Q] (hPQ : ∀ (n : ℕ), P n → Q n) (n : ℕ) :
        Nat.findGreatest P n ≤ Nat.findGreatest Q n
        source
        theorem Nat.findGreatest_mono {m : ℕ} {P Q : ℕ → Prop} [DecidablePred P] {n : ℕ} [DecidablePred Q] (hPQ : ∀ (n : ℕ), P n → Q n) (hmn : m ≤ n) :
        Nat.findGreatest P m ≤ Nat.findGreatest Q n
        source
        theorem Nat.findGreatest_is_greatest {k : ℕ} {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (hk : Nat.findGreatest P n < k) (hkb : k ≤ n) :
        ¬P k
        source
        theorem Nat.findGreatest_of_ne_zero {m : ℕ} {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (h : Nat.findGreatest P n = m) (h0 : m ≠ 0) :
        P m