mathlib3 documentation

data.pnat.find

Explicit least witnesses to existentials on positive natural numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Implemented via calling out to nat.find.

source
@[protected, instance]
def pnat.decidable_pred_exists_nat {p : ℕ+ → Prop} [decidable_pred p] :
decidable_pred (λ (n' : ℕ), ∃ (n : ℕ+) (hn : n' = ↑n), p n)
Equations
source
@[protected]
def pnat.find_x {p : ℕ+ → Prop} [decidable_pred p] (h : ∃ (n : ℕ+), p n) :
{n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m}

The pnat version of nat.find_x

Equations
source
@[protected]
def pnat.find {p : ℕ+ → Prop} [decidable_pred 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
source
@[protected]
theorem pnat.find_spec {p : ℕ+ → Prop} [decidable_pred p] (h : ∃ (n : ℕ+), p n) :
p (pnat.find h)
source
@[protected]
theorem pnat.find_min {p : ℕ+ → Prop} [decidable_pred p] (h : ∃ (n : ℕ+), p n) {m : ℕ+} :
m < pnat.find h → ¬p m
source
@[protected]
theorem pnat.find_min' {p : ℕ+ → Prop} [decidable_pred p] (h : ∃ (n : ℕ+), p n) {m : ℕ+} (hm : p m) :
pnat.find h ≤ m
source
theorem pnat.find_eq_iff {p : ℕ+ → Prop} [decidable_pred p] (h : ∃ (n : ℕ+), p n) {m : ℕ+} :
pnat.find h = m ↔ p m ∧ ∀ (n : ℕ+), n < m → ¬p n
source
@[simp]
theorem pnat.find_lt_iff {p : ℕ+ → Prop} [decidable_pred p] (h : ∃ (n : ℕ+), p n) (n : ℕ+) :
pnat.find h < n ↔ ∃ (m : ℕ+) (H : m < n), p m
source
@[simp]
theorem pnat.find_le_iff {p : ℕ+ → Prop} [decidable_pred p] (h : ∃ (n : ℕ+), p n) (n : ℕ+) :
pnat.find h ≤ n ↔ ∃ (m : ℕ+) (H : m ≤ n), p m
source
@[simp]
theorem pnat.le_find_iff {p : ℕ+ → Prop} [decidable_pred p] (h : ∃ (n : ℕ+), p n) (n : ℕ+) :
n ≤ pnat.find h ↔ ∀ (m : ℕ+), m < n → ¬p m
source
@[simp]
theorem pnat.lt_find_iff {p : ℕ+ → Prop} [decidable_pred p] (h : ∃ (n : ℕ+), p n) (n : ℕ+) :
n < pnat.find h ↔ ∀ (m : ℕ+), m ≤ n → ¬p m
source
@[simp]
theorem pnat.find_eq_one {p : ℕ+ → Prop} [decidable_pred p] (h : ∃ (n : ℕ+), p n) :
pnat.find h = 1 ↔ p 1
source
@[simp]
theorem pnat.one_le_find {p : ℕ+ → Prop} [decidable_pred p] (h : ∃ (n : ℕ+), p n) :
1 < pnat.find h ↔ ¬p 1
source
theorem pnat.find_mono {p q : ℕ+ → Prop} [decidable_pred p] [decidable_pred 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} [decidable_pred p] {n : ℕ+} {h : ∃ (n : ℕ+), p n} (hn : p n) :
pnat.find h ≤ n
source
theorem pnat.find_comp_succ {p : ℕ+ → Prop} [decidable_pred p] (h : ∃ (n : ℕ+), p n) (h₂ : ∃ (n : ℕ+), p (n + 1)) (h1 : ¬p 1) :
pnat.find h = pnat.find h₂ + 1