Explicit least witnesses to existentials on positive natural numbers #
Implemented via calling out to Nat.find
.
instance
PNat.decidablePredExistsNat
{p : ℕ+ → Prop}
[DecidablePred p]
:
DecidablePred fun n' => ∃ n x, 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:
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
.
Instances For
@[simp]
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}
: