surjective_count_of_infinite_setOf

English

If {n | p(n)} is infinite, then the counting function count p is surjective onto ℕ; in particular, for each n there exists m with count p m = n (e.g., m = nth p n).

Русский

Если множество истинности бесконечно, то функция счёта счётчика count p сюръективна на ℕ; для каждого n существует m с count p m = n (например, m = nth p n).

LaTeX

$$$$ \\left(\\{n:\\, p(n)\\}.Infinite\\right) \\Rightarrow \\text{Surjective}(\\mathrm{count}\\,p), \\quad \\forall n, \\exists m, \\mathrm{count}(p,m)=n.$$$$

Lean4

theorem surjective_count_of_infinite_setOf (h : {n | p n}.Infinite) : Function.Surjective (Nat.count p) := fun n =>
  ⟨nth p n, count_nth_of_infinite h n⟩

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