lt_opow_of_log_lt

Mathlib.SetTheory.Ordinal.Exponential

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

English

If hb = 1 < b and log b x < c, then x < b^c.

Русский

Если hb = 1 < b и log_b x < c, тогда x < b^c.

LaTeX

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

Lean4

theorem lt_opow_of_log_lt {b x c : Ordinal} (hb : 1 < b) : log b x < c → x < b ^ c :=
  lt_imp_lt_of_le_imp_le <| le_log_of_opow_le hb

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

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

Разделы

Аффилиация

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