primeCounting — Mathlib

English

The function π' counts the number of primes strictly less than the input.

Русский

Функция π' подсчитывает количество простых чисел строго меньше входного аргумента.

LaTeX

$$$$ \\pi'(n) = \\#\\{ p\\;|\\; p \\text{ prime} \\\\ p < n \\} $$$$

Lean4

/-- The prime counting function: Returns the number of primes less than or equal to the input.

With `open scoped Nat.Prime`, this has notation `π`. -/
def primeCounting (n : ℕ) : ℕ :=
  primeCounting' (n + 1)

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