le_rpow_inv_iff_of_pos — Mathlib

English

Let y ≥ 0 and z > 0. Then x ≤ y^{1/z} is equivalent to x^z ≤ y for x ≥ 0. In other words, taking a positive inverse power preserves the inequality direction when handled properly.

Русский

Пусть y ≥ 0 и z > 0. Тогда x ≤ y^{1/z} эквивалентно x^z ≤ y для x ≥ 0.

LaTeX

$$$(0 \le y) \land (0 < z) \Rightarrow x \le y^{z^{-1}} \iff x^{z} \le y$$$

Lean4

theorem le_rpow_inv_iff_of_pos (hy : 0 ≤ y) (hz : 0 < z) (x : ℝ≥0) : x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y :=
  Real.le_rpow_inv_iff_of_pos x.2 hy hz

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