rpow_le_rpow_of_exponent_le — Mathlib

English

If x ≥ 1 and y ≤ z, then x^{y} ≤ x^{z}.

Русский

Пусть x ≥ 1 и y ≤ z. Тогда x^y ≤ x^z.

LaTeX

$$$ x \\ge 1 \\;\\land\\; y \\le z \\Rightarrow x^{y} \\le x^{z} $$$

Lean4

@[gcongr]
theorem rpow_le_rpow_of_exponent_le {x : ℝ≥0∞} {y z : ℝ} (hx : 1 ≤ x) (hyz : y ≤ z) : x ^ y ≤ x ^ z :=
  by
  cases x
  ·
    rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;> rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
        simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos, le_refl] <;>
      linarith
  · simp only [one_le_coe_iff] at hx
    simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)), NNReal.rpow_le_rpow_of_exponent_le hx hyz]

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