rpow_inv_rpow

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#ENNReal.rpow_inv_rpow

English

If x ∈ ENNReal with 0 < x and x ≤ 1 and z < 0, then 1 ≤ x^{z}.

Русский

Если x > 0 и x ≤ 1 и z < 0, тогда 1 ≤ x^z.

LaTeX

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

Lean4

@[simp]
theorem rpow_inv_rpow {y : ℝ} (hy : y ≠ 0) (x : ℝ≥0∞) : (x ^ y⁻¹) ^ y = x := by
  rw [← rpow_mul, inv_mul_cancel₀ hy, rpow_one]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru