rpow_le_rpow_of_exponent_ge' — Mathlib

English

If 0 ≤ x ≤ 1, 0 ≤ z ≤ y, then x^y ≤ x^z.

Русский

Если 0 ≤ x ≤ 1, 0 ≤ z ≤ y, то x^y ≤ x^z.

LaTeX

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

Lean4

/-- This version of `rpow_le_rpow_of_exponent_ge` allows `x = 0` but requires `0 ≤ z`.
See also `rpow_le_rpow_of_exponent_ge_of_imp` for the most general version. -/
theorem rpow_le_rpow_of_exponent_ge' (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hz : 0 ≤ z) (hyz : z ≤ y) : x ^ y ≤ x ^ z :=
  rpow_le_rpow_of_exponent_ge_of_imp hx0 hx1 hyz fun _ hy ↦ le_antisymm (hyz.trans_eq hy) hz

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