rpow_lt_rpow_of_exponent_gt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem rpow_lt_rpow_of_exponent_gt {x : ℝ≥0∞} {y z : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) : x ^ y < x ^ z :=
  by
  lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx1 le_top)
  simp only [coe_lt_one_iff, coe_pos] at hx0 hx1
  simp [← coe_rpow_of_ne_zero (ne_of_gt hx0), NNReal.rpow_lt_rpow_of_exponent_gt hx0 hx1 hyz]

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