surjective_primeCounting — Mathlib

English

The prime-counting function π is surjective: for every m in N there exists n in N with π(n) = m.

Русский

Функция подсчета простых π сюръективна по отношению к натуральным числам: для каждого m существует n, такое что π(n) = m.

LaTeX

$$$\forall m \in \mathbb{N}, \exists n \in \mathbb{N}, \pi(n) = m$$$

Lean4

theorem surjective_primeCounting : Function.Surjective π :=
  by
  suffices Function.Surjective (π ∘ fun n => n - 1) from this.of_comp
  convert surjective_primeCounting'
  ext
  exact primeCounting_sub_one _

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