le_rpow_inv_iff — Mathlib

English

For x,y ∈ ENNReal and z > 0, x ≤ y^{z^{-1}} iff x^z ≤ y.

Русский

Для x,y ∈ ENNReal и z > 0 верно x ≤ y^{z^{-1}} iff x^z ≤ y.

LaTeX

$$$$ x \le y^{z^{-1}} \;\Leftrightarrow\; x^{z} \le y \quad (z>0). $$$$

Lean4

theorem le_rpow_inv_iff {x y : ℝ≥0∞} {z : ℝ} (hz : 0 < z) : x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y :=
  by
  nth_rw 1 [← rpow_one x]
  nth_rw 1 [← @mul_inv_cancel₀ _ _ z hz.ne']
  rw [rpow_mul, @rpow_le_rpow_iff _ _ z⁻¹ (by simp [hz])]

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