le_pow_clog

Mathlib.Data.Nat.Log

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

English

For any b > 1 and x, we have x ≤ b^{clog_b(x)}.

Русский

Пусть b > 1 и x. Тогда x ≤ b^{clog_b(x)}.

LaTeX

$$$ x \\le b^{\\operatorname{clog}_b x} \\quad (1 < b) $$$

Lean4

theorem le_pow_clog {b : ℕ} (hb : 1 < b) (x : ℕ) : x ≤ b ^ clog b x :=
  (clog_le_iff_le_pow hb).1 le_rfl

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

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

Разделы

Аффилиация

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