rpow_lt_rpow

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

If x < y and z > 0, then x^z < y^z for x,y ≥ 0 and z ∈ ℝ.

Русский

Если x < y и z > 0, то x^z < y^z для x,y ≥ 0 и z ∈ ℝ.

LaTeX

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

Lean4

@[gcongr]
theorem rpow_lt_rpow {x y : ℝ≥0} {z : ℝ} (h₁ : x < y) (h₂ : 0 < z) : x ^ z < y ^ z :=
  Real.rpow_lt_rpow x.2 h₁ h₂

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

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

Разделы

Аффилиация

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