rpow_le_rpow_of_exponent_le — Mathlib

English

If 1 ≤ x and y ≤ z, then x^y ≤ x^z. For base at least 1, exponent increases yield nondecreasing power.

Русский

Если x ≥ 1 и y ≤ z, то x^y ≤ x^z. Для базы не меньше 1 показатель возрастает неубывающе.

LaTeX

$$$x ≥ 1 \land y ≤ z \Rightarrow x^{y} ≤ 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 :=
  Real.rpow_le_rpow_of_exponent_le hx hyz

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