count_nth_succ_of_infinite — Mathlib

English

If the truth-set {n | p(n)} is infinite, then for every n, count p (nth p n + 1) = n + 1.

Русский

Если множество истинности бесконечно, то для каждого n выполняется count p (nth p n + 1) = n + 1.

LaTeX

$$$$ \\forall n:\\mathbb{N}, \\; \\mathrm{count}(p, \\mathrm{nth}(p, n) + 1) = n + 1.$$$$

Lean4

theorem count_nth_succ_of_infinite (hp : (setOf p).Infinite) (n : ℕ) : count p (nth p n + 1) = n + 1 := by
  rw [count_succ, count_nth_of_infinite hp, if_pos (nth_mem_of_infinite hp _)]

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