clog_eq_one

Mathlib.Data.Nat.Log

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem clog_eq_one {b n : ℕ} (hn : 2 ≤ n) (h : n ≤ b) : clog b n = 1 :=
  by
  rw [clog_of_two_le (hn.trans h) hn, clog_of_right_le_one]
  rw [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul] <;> omega

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

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

Разделы

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

Аффилиация

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