pow_lt_of_lt_log

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Real.pow_lt_of_lt_log

English

If 0 < y and log x < z log y, then x < y^z.

Русский

Если 0 < y и log x < z log y, тогда x < y^z.

LaTeX

$$$0 < y \land \log x < z \log y \Rightarrow x < y^z$$$

Lean4

theorem pow_lt_of_lt_log (hy : 0 < y) (h : log x < n * log y) : x < y ^ n :=
  rpow_natCast _ _ ▸ rpow_lt_of_lt_log hy h

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

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

Разделы

Аффилиация

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