monotone_primeCounting

Mathlib.NumberTheory.PrimeCounting

URI: https://scilib.ai/kg/mathlib#Nat.monotone_primeCounting

English

The prime counting function π(n) is monotone: if m ≤ n then π(m) ≤ π(n).

Русский

Функция подсчёта простых π(n) монотонна: если m ≤ n, то π(m) ≤ π(n).

LaTeX

$$$$ m \\le n \\Rightarrow \\pi(m) \\le \\pi(n) $$$$

Lean4

theorem monotone_primeCounting : Monotone primeCounting :=
  monotone_primeCounting'.comp (monotone_id.add_const _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru