le_nth_count — Mathlib

English

If p holds for infinitely many n, then for every n, n ≤ nth p (count p n).

Русский

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

LaTeX

$$$$ \\text{If } (\\{n:\\, p(n)\\}.Infinite) \\Rightarrow \\forall n:\\, \\; n \\le \\mathrm{nth}(p, \\mathrm{count}(p,n)). $$$$

Lean4

theorem le_nth_count (hp : (setOf p).Infinite) (n : ℕ) : n ≤ nth p (count p n) :=
  let ⟨m, hp, hn⟩ := hp.exists_gt n
  le_nth_count' ⟨m, hp, hn.le⟩

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