rpow_neg — Mathlib

English

For x ≥ 0 and any y, x^(-y) = (x^y)^{-1}. (Equivalent formulation of the previous statement.)

Русский

Для x ≥ 0 и любого y верно x^{-y} = (x^{y})^{-1}.

LaTeX

$$$x \ge 0 \Rightarrow \forall y \in \mathbb{R},\ x^{-y} = (x^{y})^{-1}$$$

Lean4

/-- See also `rpow_neg_eq_inv_rpow` for a version with `x⁻¹ ^ y` in the RHS. -/
theorem rpow_neg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : x ^ (-y) = (x ^ y)⁻¹ := by simp only [rpow_def_of_nonneg hx];
  split_ifs <;> simp_all [exp_neg]

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