lt_rpow_inv_iff_of_pos

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

For hy ≥ 0 and hz > 0, x < y^{1/z} is equivalent to x^z < y for x ≥ 0, y ≥ 0.

Русский

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

LaTeX

$$$(hy : 0 \le y) (hz : 0 < z) (x : \mathbb{R}_{\ge 0}) \Rightarrow x < y^{z^{-1}} \iff x^{z} < y$$$

Lean4

theorem lt_rpow_inv_iff_of_pos (hy : 0 ≤ y) (hz : 0 < z) (x : ℝ≥0) : x < y ^ z⁻¹ ↔ x ^ z < y :=
  Real.lt_rpow_inv_iff_of_pos x.2 hy hz

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

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

Разделы

Аффилиация

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