English
If the set {k ∈ ℕ : p(k)} is finite, then the range of nth p equals {0} ∪ {k ∈ ℕ : p(k)}, i.e., it consists of 0 and exactly the p-satisfied values.
Русский
Если множество {k ∈ ℕ : p(k)} конечное, то диапазон nth p равен {0} ∪ {k ∈ ℕ : p(k)}, то есть состоит из 0 и точно тех значений, для которых p(k) выполняется.
LaTeX
$$If hf is finite, then Set.range (nth p) = insert 0 (setOf p).$$
Lean4
/-- Find the `n`-th natural number satisfying `p` (indexed from `0`, so `nth p 0` is the first
natural number satisfying `p`), or `0` if there is no such number. See also
`Subtype.orderIsoOfNat` for the order isomorphism with ℕ when `p` is infinitely often true. -/
noncomputable def nth (p : ℕ → Prop) (n : ℕ) : ℕ := by
classical
exact
if h : Set.Finite (setOf p) then (h.toFinset.sort (· ≤ ·)).getD n 0
else @Nat.Subtype.orderIsoOfNat (setOf p) (Set.Infinite.to_subtype h) n
