rpow_inv_lt_iff_of_pos

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

For x > 0, y > 0 and z < 0, x^{1/z} < y is equivalent to y < x^{z}. The negative exponent inverts the direction again.

Русский

Пусть 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 rpow_inv_lt_iff_of_pos (hy : 0 ≤ y) (hz : 0 < z) (x : ℝ≥0) : x ^ z⁻¹ < y ↔ x < y ^ z :=
  Real.rpow_inv_lt_iff_of_pos x.2 hy hz

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

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

Разделы

Аффилиация

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