range_nth_of_infinite — Mathlib

English

For any predicate p with infinite setOf p, the range of nth p equals the setOf p.

Русский

Для любого pWith бесконечно множество setOf p, диапазон функции nth p совпадает с setOf p.

LaTeX

$$$\\forall {p : \\mathbb{N} \\to \\mathbb{P}}, (\\{ n \\in \\mathbb{N} \\mid p(n) \\} \\text{ Infinite}) \\Rightarrow \\operatorname{Set.range}(\\operatorname{nth} p) = \\{ n \\in \\mathbb{N} \\mid p(n) \\}$$$

Lean4

theorem range_nth_of_infinite (hf : (setOf p).Infinite) : Set.range (nth p) = setOf p :=
  by
  rw [nth_eq_orderIsoOfNat hf]
  haveI := hf.to_subtype
  classical exact Nat.Subtype.coe_comp_ofNat_range

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