rpow_of_add_eq — Mathlib

English

Let x ∈ ℝ≥0 and w,y,z ∈ ℝ with w ≠ 0 and w = y+z. Then x^w = x^y · x^z.

Русский

Пусть x ∈ ℝ≥0 и w,y,z ∈ ℝ причём w ≠ 0 и w = y+z. Тогда x^w = x^y · x^z.

LaTeX

$$$$ \\forall x\\in\\mathbb{R}_{\\ge 0},\\ w,y,z\\in\\mathbb{R}:\\ w\\neq 0\\land w=y+z\\Rightarrow x^{\,w}=x^{\,y}x^{\,z}. $$$$

Lean4

/-- Variant of `NNReal.rpow_add'` that avoids having to prove `y + z = w` twice. -/
theorem rpow_of_add_eq (x : ℝ≥0) (hw : w ≠ 0) (h : y + z = w) : x ^ w = x ^ y * x ^ z := by rw [← h, rpow_add']; rwa [h]

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