le_pow_iff_clog_le

Mathlib.Data.Nat.Log

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

← MathLib Explorer

English

Let hb: 1 < b. Then y < clog b x iff b^y < x.

Русский

Пусть 1 < b. Тогда y < clog_b(x) эквивално b^y < x.

LaTeX

$$$ (1 < b) \Rightarrow y < \operatorname{clog}(b,x) \iff b^y < x $$$

Lean4

@[deprecated clog_le_iff_le_pow (since := "2025-10-05")]
theorem le_pow_iff_clog_le {b : ℕ} (hb : 1 < b) {x y : ℕ} : x ≤ b ^ y ↔ clog b x ≤ y :=
  (clog_le_iff_le_pow hb).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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