lt_clog_iff_pow_lt

Mathlib.Data.Nat.Log

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

English

Let hb: 1 < b. Then y < clog b x ↔ 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

theorem lt_clog_iff_pow_lt {b : ℕ} (hb : 1 < b) {x y : ℕ} : y < clog b x ↔ b ^ y < x :=
  lt_iff_lt_of_le_iff_le (clog_le_iff_le_pow hb)

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

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

Разделы

Аффилиация

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