rpow_le_rpow

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#ENNReal.rpow_le_rpow

English

For x ≤ y in ENNReal and z ≥ 0, x^z ≤ y^z.

Русский

Для x ≤ y в ENNReal и z ≥ 0 выполняется x^z ≤ y^z.

LaTeX

$$$$ x \le y \;\Rightarrow\; 0 \le z \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 :=
  monotone_rpow_of_nonneg h₂ h₁

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

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

Разделы

Аффилиация

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