lt_rpow_inv_iff — Mathlib

English

Let x, y be ENNReal and z > 0. Then x < y^{z^{-1}} if and only if x^{z} < y.

Русский

Пусть x, y ∈ ENNReal и z > 0. Тогда x < y^{1/z} тогда и только тогда, когда x^{z} < y.

LaTeX

$$$ x < y^{z^{-1}} \\iff x^{z} < y $$$

Lean4

theorem lt_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 (ne_of_lt hz).symm]
  rw [rpow_mul, @rpow_lt_rpow_iff _ _ z⁻¹ (by simp [hz])]

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