rpow_lt_rpow_iff_of_neg — Mathlib

English

For x > 0, y > 0 and z < 0, we have x^z < y^z if and only if y < x. The power with a negative exponent reverses the order.

Русский

Пусть x > 0, y > 0 и z < 0. Тогда x^z < y^z тогда и только тогда, когда y < x. Степень с отрицательным показателем обращает порядок.

LaTeX

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

Lean4

theorem rpow_lt_rpow_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x ^ z < y ^ z ↔ y < x :=
  Real.rpow_lt_rpow_iff_of_neg hx hy hz

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