monotone_rpow_of_nonneg — Mathlib

English

If z ≥ 0, the map x ↦ x^z is monotone on ℝ≥0.

Русский

Если z ≥ 0, отображение x ↦ x^z на ℝ≥0 монотонно.

LaTeX

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

Lean4

theorem monotone_rpow_of_nonneg {z : ℝ} (h : 0 ≤ z) : Monotone fun x : ℝ≥0 => x ^ z :=
  h.eq_or_lt.elim (fun h0 => h0 ▸ by simp only [rpow_zero, monotone_const]) fun h0 =>
    (strictMono_rpow_of_pos h0).monotone

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