inv_rpow

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Real.inv_rpow

English

If x ≥ 0, then x^{-1})^y = (x^y)^{-1}.

Русский

Пусть x ≥ 0, тогда (x^{-1})^y = (x^y)^{-1}.

LaTeX

$$$\\\\forall x \\\\ge 0, \\\\forall y: \ x^{-1})^y = (x^y)^{-1}.$$$

Lean4

theorem inv_rpow (hx : 0 ≤ x) (y : ℝ) : x⁻¹ ^ y = (x ^ y)⁻¹ := by rw [← rpow_neg_eq_inv_rpow, rpow_neg hx]

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

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

Разделы

Аффилиация

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