PNat.find_min'
theorem PNat.find_min' : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) {m : ℕ+}, p m → PNat.find h ≤ m := by
sorry
The theorem `PNat.find_min'` states that for any decidable predicate `p` on positive natural numbers (`ℕ+`), given the existence of a positive natural number `n` that satisfies the predicate `p` (notated as `p n`), and any positive natural number `m` such that `p m` holds, the function `PNat.find h`, which finds the smallest positive natural number satisfying the predicate `p`, always returns a value that is less than or equal to `m`.
More concisely: For any decidable predicate `p` on positive natural numbers, if there exists a positive natural number `n` such that `p n` holds and `m` is any positive natural number with `p m` holding, then `PNat.find h` returns a value less than or equal to `m`.
|
PNat.find_spec
theorem PNat.find_spec : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n), p (PNat.find h)
The theorem `PNat.find_spec` states that for every predicate `p` on positive natural numbers, given that the predicate `p` is decidable (meaning, for each positive natural number, we can decide whether `p` holds or not), if there exists at least one positive natural number for which the predicate `p` holds, then the predicate `p` also holds for the positive natural number obtained by applying the function `PNat.find` to the proof of existence. In other words, `PNat.find` delivers a positive natural number that satisfies the predicate `p`.
More concisely: If `p` is a decidable predicate on positive natural numbers with at least one positive natural number satisfying `p`, then `p` holds for the number `PNat.find p`.
|