monotone_primeCounting'

Mathlib.NumberTheory.PrimeCounting

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

English

The function π' is monotone with respect to the natural order: if m ≤ n then π'(m) ≤ π'(n).

Русский

Функция π' монотонна по отношению к естественному порядку: если m ≤ n, то π'(m) ≤ π'(n).

LaTeX

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

Lean4

theorem monotone_primeCounting' : Monotone primeCounting' :=
  count_monotone Prime

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

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

Разделы

Аффилиация

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