inv_rpow — Mathlib

English

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

Русский

Для x ∈ ENNReal и y ∈ ℝ выполнено (x^{-1})^{y} = (x^{y})^{-1}.

LaTeX

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

Lean4

theorem inv_rpow (x : ℝ≥0∞) (y : ℝ) : x⁻¹ ^ y = (x ^ y)⁻¹ :=
  by
  rcases eq_or_ne y 0 with (rfl | hy); · simp only [rpow_zero, inv_one]
  replace hy := hy.lt_or_gt
  rcases eq_or_ne x 0 with (rfl | h0); · cases hy <;> simp [*]
  rcases eq_or_ne x ⊤ with (rfl | h_top); · cases hy <;> simp [*]
  apply ENNReal.eq_inv_of_mul_eq_one_left
  rw [← mul_rpow_of_ne_zero (ENNReal.inv_ne_zero.2 h_top) h0, ENNReal.inv_mul_cancel h0 h_top, one_rpow]

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