rpow_le_rpow

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#NNReal.rpow_le_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 \le y \land z \ge 0 \Rightarrow x^{z} \le y^{z}$$

Lean4

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

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

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

Разделы

Аффилиация

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