range_nth_subset — Mathlib

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 _ _)

Похожие утверждения