rpow_le_rpow_iff_of_neg

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

For x > 0, y > 0 and z < 0, x^z ≤ y^z if and only if y ≤ x. Again, negative exponents reverse order.

Русский

Пусть x > 0, y > 0 и z < 0. Тогда x^z ≤ y^z тогда и только тогда, когда y ≤ x.

LaTeX

$$$0 < x \land 0 < y \land z < 0 \Rightarrow x^{z} \le y^{z} \iff y \le x$$$

Lean4

theorem rpow_le_rpow_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x ^ z ≤ y ^ z ↔ y ≤ x :=
  Real.rpow_le_rpow_iff_of_neg hx hy hz

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

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

Разделы

Аффилиация

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