rpow_lt_rpow_of_exponent_neg — Mathlib

English

If hy > 0, y < x, and hz < 0, then x^z < y^z.

Русский

Если hy > 0, y < x, и hz < 0, то x^z < y^z.

LaTeX

$$$ (0

Lean4

theorem rpow_lt_rpow_of_exponent_neg {x y z : ℝ} (hy : 0 < y) (hxy : y < x) (hz : z < 0) : x ^ z < y ^ z :=
  by
  have hx : 0 < x := hy.trans hxy
  rw [← neg_neg z, Real.rpow_neg (le_of_lt hx) (-z), Real.rpow_neg (le_of_lt hy) (-z),
    inv_lt_inv₀ (rpow_pos_of_pos hx _) (rpow_pos_of_pos hy _)]
  exact Real.rpow_lt_rpow (by positivity) hxy <| neg_pos_of_neg hz

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