lt_rpow_inv_iff_of_neg

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

For x > 0, y > 0 and z < 0, x^{1/z} < y ⇔ y < x^{z}. The inequality direction is reversed by negating the exponent.

Русский

Пусть x > 0, y > 0 и z < 0. Тогда x^{1/z} < y эквивалентно y < x^{z}.

LaTeX

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

Lean4

theorem lt_rpow_inv_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x < y ^ z⁻¹ ↔ y < x ^ z :=
  Real.lt_rpow_inv_iff_of_neg hx hy hz

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

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

Разделы

Аффилиация

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