Documentation

Mathlib.Data.PNat.Find

Explicit least witnesses to existentials on positive natural numbers #

Implemented via calling out to Nat.find.

source
instance PNat.decidablePredExistsNat {p : ℕ+ → Prop} [DecidablePred p] :
DecidablePred fun (n' : ℕ) => ∃ (n : ℕ+) (_ : n' = ↑n), p n
Equations
  • One or more equations did not get rendered due to their size.
source
def PNat.findX {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) :
{ n : ℕ+ // p n ∧ ∀ m < n, ¬p m }

The PNat version of Nat.findX

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def PNat.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 positive natural number satisfying p, then PNat.find hp is the smallest positive natural number satisfying p. Note that PNat.find is protected, meaning that you can't just write find, even if the PNat namespace is open.

    The API for PNat.find is:

    Equations
    Instances For
      source
      theorem PNat.find_spec {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) :
      p (PNat.find h)
      source
      theorem PNat.find_min {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) {m : ℕ+} :
      m < PNat.find h → ¬p m
      source
      theorem PNat.find_min' {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) {m : ℕ+} (hm : p m) :
      PNat.find h ≤ m
      source
      theorem PNat.find_eq_iff {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) {m : ℕ+} :
      PNat.find h = m ↔ p m ∧ ∀ n < m, ¬p n
      source
      @[simp]
      theorem PNat.find_lt_iff {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) (n : ℕ+) :
      PNat.find h < n ↔ ∃ m < n, p m
      source
      @[simp]
      theorem PNat.find_le_iff {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) (n : ℕ+) :
      PNat.find h ≤ n ↔ ∃ m ≤ n, p m
      source
      @[simp]
      theorem PNat.le_find_iff {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) (n : ℕ+) :
      n ≤ PNat.find h ↔ ∀ m < n, ¬p m
      source
      @[simp]
      theorem PNat.lt_find_iff {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) (n : ℕ+) :
      n < PNat.find h ↔ ∀ m ≤ n, ¬p m
      source
      @[simp]
      theorem PNat.find_eq_one {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) :
      PNat.find h = 1 ↔ p 1
      source
      theorem PNat.one_le_find {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) :
      1 < PNat.find h ↔ ¬p 1
      source
      theorem PNat.find_mono {p : ℕ+ → Prop} {q : ℕ+ → Prop} [DecidablePred p] [DecidablePred q] (h : ∀ (n : ℕ+), q n → p n) {hp : ∃ (n : ℕ+), p n} {hq : ∃ (n : ℕ+), q n} :
      PNat.find hp ≤ PNat.find hq
      source
      theorem PNat.find_le {p : ℕ+ → Prop} [DecidablePred p] {n : ℕ+} {h : ∃ (n : ℕ+), p n} (hn : p n) :
      PNat.find h ≤ n
      source
      theorem PNat.find_comp_succ {p : ℕ+ → Prop} [DecidablePred p] (h : ∃ (n : ℕ+), p n) (h₂ : ∃ (n : ℕ+), p (n + 1)) (h1 : ¬p 1) :
      PNat.find h = PNat.find h₂ + 1