English
If there exists n with p(n), then there exists a decidable predicate on ℕ that decides membership of n' as a witness n with p(n).
Русский
Если существует n с p(n), то существует решаемый предикат на ℕ, который определяет, является ли n' кодом свидетеля p(n).
LaTeX
$$$ \\exists q:\\\\mathbb{N} \\to \\mathsf{Prop},\\; \\text{DecidablePred}(q) \\land \\forall n'\\; q(n') \\iff \\exists n:\\mathbb{N}^+,\\; n' = n \\land p(n). $$$
Lean4
instance decidablePredExistsNat : DecidablePred fun n' : ℕ => ∃ (n : ℕ+) (_ : n' = n), p n := fun n' =>
decidable_of_iff' (∃ h : 0 < n', p ⟨n', h⟩) <|
Subtype.exists.trans <| by simp_rw [mk_coe, @exists_comm (_ < _) (_ = _), exists_prop, exists_eq_left']
