Explicit least witnesses to existentials on positive natural numbers #
Implemented via calling out to nat.find
.
@[protected, instance]
def
pnat.decidable_pred_exists_nat
{p : ℕ+ → Prop}
[decidable_pred p] :
decidable_pred (λ (n' : ℕ), ∃ (n : ℕ+) (hn : n' = ↑n), p n)
Equations
- pnat.decidable_pred_exists_nat = λ (n' : ℕ), decidable_of_iff' (∃ (h : 0 < n'), p ⟨n', h⟩) _
@[protected]
The pnat
version of nat.find_x
Equations
- pnat.find_x h = ⟨⟨↑(nat.find_x _), _⟩, _⟩
@[protected]
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:
pnat.find_spec
is the proof thatpnat.find hp
satisfiesp
.pnat.find_min
is the proof that ifm < pnat.find hp
thenm
does not satisfyp
.pnat.find_min'
is the proof that ifm
does satisfyp
thenpnat.find hp ≤ m
.
Equations
- pnat.find h = ↑(pnat.find_x h)
@[protected]
@[protected]
@[protected]
theorem
pnat.find_min'
{p : ℕ+ → Prop}
[decidable_pred p]
(h : ∃ (n : ℕ+), p n)
{m : ℕ+}
(hm : p m) :
@[simp]
@[simp]
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} :