tendsto_primeCounting' — Mathlib

English

The function π' tends to infinity as its input goes to infinity; i.e., π'(n) grows without bound.

Русский

Функция π' бесконечно возрастает при увеличении аргумента: π'(n) неограниченно растет когда n → ∞.

LaTeX

$$$\lim_{n \to \infty} \pi'(n) = \infty$$$

Lean4

theorem tendsto_primeCounting' : Tendsto π' atTop atTop :=
  by
  apply tendsto_atTop_atTop_of_monotone' monotone_primeCounting'
  simp [Set.range_eq_univ.mpr surjective_primeCounting']

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