rpow_le_rpow_of_nonpos — Mathlib

English

If 0 < x and x ≤ y and z ≤ 0, then y^z ≤ x^z. In words, for a fixed nonpositive exponent z, the function t ↦ t^z is order-reversing on (0, ∞).

Русский

Пусть x > 0, x ≤ y и z ≤ 0. Тогда y^z ≤ x^z. Иными словами, для фиксированного не положительного показателя z функция t ↦ t^z убывающая на (0, ∞).

LaTeX

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

Lean4

theorem rpow_le_rpow_of_nonpos (hx : 0 < x) (hxy : x ≤ y) (hz : z ≤ 0) : y ^ z ≤ x ^ z :=
  Real.rpow_le_rpow_of_nonpos hx hxy hz

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