surjective_primeCounting' — Mathlib

English

π' is a surjective function: for every m in N there exists n in N with π'(n) = m.

Русский

π' отображает множество всех натуральных чисел на все naturals: для каждого m найдется n such that π'(n) = m.

LaTeX

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

Lean4

theorem surjective_primeCounting' : Function.Surjective π' :=
  Nat.surjective_count_of_infinite_setOf infinite_setOf_prime

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