rpow_lt_one_of_one_lt_of_neg

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#ENNReal.rpow_lt_one_of_one_lt_of_neg

← MathLib Explorer

English

If x > 1 and z < 0, then x^{z} < 1.

Русский

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

LaTeX

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

Lean4

theorem rpow_lt_one_of_one_lt_of_neg {x : ℝ≥0∞} {z : ℝ} (hx : 1 < x) (hz : z < 0) : x ^ z < 1 :=
  by
  cases x
  · simp [top_rpow_of_neg hz, zero_lt_one]
  · simp only [one_lt_coe_iff] at hx
    simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_trans zero_lt_one hx)), NNReal.rpow_lt_one_of_one_lt_of_neg hx hz]

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

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

Разделы

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

Аффилиация

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