rpow_sub

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

← MathLib Explorer

English

Let x > 0. For y,z ∈ ℝ, x^(y−z) = x^y / x^z.

Русский

Пусть x > 0. Пусть y,z ∈ ℝ. Тогда x^(y−z) = x^y / x^z.

LaTeX

$$$$ \\forall x>0,\\ \\forall y,z\\in\\mathbb{R},\\ x^{\,y-z}=\\dfrac{x^{\,y}}{x^{\,z}}. $$$$

Lean4

theorem rpow_sub {x : ℝ≥0} (hx : x ≠ 0) (y z : ℝ) : x ^ (y - z) = x ^ y / x ^ z :=
  NNReal.eq <| Real.rpow_sub ((NNReal.coe_pos.trans pos_iff_ne_zero).mpr hx) y z

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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