one_lt_rpow

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#NNReal.one_lt_rpow

English

If 1 < x and z > 0, then 1 < x^z. Base greater than 1 with positive exponent yields a number greater than 1.

Русский

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

LaTeX

$$$1 < x \land z > 0 \Rightarrow 1 < x^{z}$$$

Lean4

theorem one_lt_rpow {x : ℝ≥0} {z : ℝ} (hx : 1 < x) (hz : 0 < z) : 1 < x ^ z :=
  Real.one_lt_rpow hx hz

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

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

Разделы

Аффилиация

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