rpow_neg — Mathlib

English

For ENNReal x and any y, x^(-y) = (x^y)^{-1}.

Русский

Для ENNReal x и любого y: x^(-y) = (x^y)^{-1}.

LaTeX

$$$x^{(-y)} = (x^{y})^{-1}$$$

Lean4

theorem rpow_neg (x : ℝ≥0∞) (y : ℝ) : x ^ (-y) = (x ^ y)⁻¹ := by
  cases x with
  | top => rcases lt_trichotomy y 0 with (H | H | H) <;> simp [top_rpow_of_pos, top_rpow_of_neg, H, neg_pos.mpr]
  | coe x =>
    by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;> simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]
    · have A : x ^ y ≠ 0 := by simp [h]
      simp [← coe_rpow_of_ne_zero h, ← coe_inv A, NNReal.rpow_neg]

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