rpow_add_of_add_pos — Mathlib

English

For ENNReal x and y,z with y≥0, z≥0, x^(y+z) = x^y · x^z.

Русский

Для ENNReal x и y,z с y≥0, z≥0: x^(y+z) = x^y · x^z.

LaTeX

$$$y \\ge 0,\\ z \\ge 0 \\Rightarrow x^{y+z} = x^{y} \\cdot x^{z}$$$

Lean4

theorem rpow_add_of_add_pos {x : ℝ≥0∞} (hx : x ≠ ⊤) (y z : ℝ) (hyz : 0 < y + z) : x ^ (y + z) = x ^ y * x ^ z :=
  by
  obtain (rfl | hx') := eq_or_ne x 0
  · by_cases hy' : 0 < y
    · simp [ENNReal.zero_rpow_of_pos hyz, ENNReal.zero_rpow_of_pos hy']
    · have hz' : 0 < z := by linarith
      simp [ENNReal.zero_rpow_of_pos hyz, ENNReal.zero_rpow_of_pos hz']
  · rw [ENNReal.rpow_add _ _ hx' hx]

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