rpow_neg

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#NNReal.rpow_neg

English

For x ∈ NNReal and y ∈ Real, x^{−y} = (x^y)^{−1}.

Русский

Для x ∈ ℝ≥0 и y ∈ ℝ: x^{−y} = (x^y)^{−1}.

LaTeX

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

Lean4

theorem rpow_neg (x : ℝ≥0) (y : ℝ) : x ^ (-y) = (x ^ y)⁻¹ :=
  NNReal.eq <| Real.rpow_neg x.2 _

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

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

Разделы

Аффилиация

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