rpow_lt_rpow_iff

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

If z > 0, then x^z < y^z ↔ x < y for x,y ≥ 0.

Русский

Если z > 0, то x^z < y^z ↔ x < y при x,y ≥ 0.

LaTeX

$$z > 0 \Rightarrow (x^{z} < y^{z} \Leftrightarrow x < y)$$

Lean4

theorem rpow_lt_rpow_iff {x y : ℝ≥0} {z : ℝ} (hz : 0 < z) : x ^ z < y ^ z ↔ x < y :=
  Real.rpow_lt_rpow_iff x.2 y.2 hz

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

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

Разделы

Аффилиация

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