strictMono_rpow_of_pos

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

For z > 0, the map x ↦ x^z is strictly monotone on ℝ≥0.

Русский

Для z > 0 отображение x ↦ x^z на ℝ≥0 строго монотоно.

LaTeX

$$$z > 0 \\Rightarrow \\text{StrictMono}(\\lambda x: \\mathbb{R}_{\\ge 0} \\; x \\mapsto x^z)$$$

Lean4

theorem strictMono_rpow_of_pos {z : ℝ} (h : 0 < z) : StrictMono fun x : ℝ≥0 => x ^ z := fun x y hxy => by
  simp only [NNReal.rpow_lt_rpow hxy h]

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

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

Разделы

Аффилиация

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