div_opow_log_lt

Mathlib.SetTheory.Ordinal.Exponential

URI: https://scilib.ai/kg/mathlib#Ordinal.div_opow_log_lt

← MathLib Explorer

English

For hb > 1 and o > 0, o / (b^{log_b o}) < b.

Русский

При hb > 1 и o > 0 имеет место: o / (b^{log_b o}) < b.

LaTeX

$$$ \dfrac{o}{b^{\log_b o}} < b $$$

Lean4

theorem div_opow_log_lt {b : Ordinal} (o : Ordinal) (hb : 1 < b) : o / (b ^ log b o) < b :=
  by
  rw [div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ← opow_succ]
  exact lt_opow_succ_log_self hb o

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

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

Разделы

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

Аффилиация

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