English
For any p, the range of nth p is contained in the set {0} ∪ {x : p x}.
Русский
Для любого p образ диапазона nth p лежит в {0} ∪ {x | p x}.
LaTeX
$$$\\\\mathrm{range}(\\\\mathrm{nth}\\\\ p)\\\\subseteq\\\\{0\\\\}\\\\cup\\\\{x:\\\\mathbb{N}\\\\mid p x\\\\}.$$$
Lean4
theorem range_nth_subset : Set.range (nth p) ⊆ insert 0 (setOf p) :=
(setOf p).finite_or_infinite.elim (fun h => (range_nth_of_finite h).subset) fun h =>
(range_nth_of_infinite h).trans_subset (Set.subset_insert _ _)