strictMono_rpow_of_pos — Mathlib

English

If z > 0, then the map x → x^z is strictly increasing on ENNReal; i.e., x < y implies x^z < y^z.

Русский

Если z > 0, то отображение x → x^z строго возрастает на ENNReal; то есть x < y ⇒ x^z < y^z.

LaTeX

$$$$ ext{If } z > 0, \; x < y \; \Rightarrow \; x^{z} < y^{z}.$$$$

Lean4

theorem strictMono_rpow_of_pos {z : ℝ} (h : 0 < z) : StrictMono fun x : ℝ≥0∞ => x ^ z :=
  by
  intro x y hxy
  lift x to ℝ≥0 using ne_top_of_lt hxy
  rcases eq_or_ne y ∞ with (rfl | hy)
  · simp only [top_rpow_of_pos h, ← coe_rpow_of_nonneg _ h.le, coe_lt_top]
  · lift y to ℝ≥0 using hy
    simp only [← coe_rpow_of_nonneg _ h.le, NNReal.rpow_lt_rpow (coe_lt_coe.1 hxy) h, coe_lt_coe]

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