lt_log_of_lt_opow

Mathlib.SetTheory.Ordinal.Exponential

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

English

If c ≠ 0 and x < b^c, then log b x < c.

Русский

Если c ≠ 0 и x < b^c, то log_b x < c.

LaTeX

$$$ x < b^c \Rightarrow \log_b x < c $$$

Lean4

theorem lt_log_of_lt_opow {b x c : Ordinal} (hc : c ≠ 0) : x < b ^ c → log b x < c :=
  lt_imp_lt_of_le_imp_le <| opow_le_of_le_log hc

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

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

Разделы

Аффилиация

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