rpow_add — Mathlib

English

For ENNReal x ≠ 0 and x ≠ ∞, x^(y+z) = x^y · x^z.

Русский

Для ENNReal x ≠ 0 и x ≠ ∞: x^(y+z) = x^y · x^z.

LaTeX

$$$x \\neq 0 \\land x \\neq \\infty \\Rightarrow x^{y+z} = x^{y} \\cdot x^{z}$$$

Lean4

theorem rpow_add {x : ℝ≥0∞} (y z : ℝ) (hx : x ≠ 0) (h'x : x ≠ ⊤) : x ^ (y + z) = x ^ y * x ^ z := by
  cases x with
  | top => exact (h'x rfl).elim
  | coe x =>
    have : x ≠ 0 := fun h => by simp [h] at hx
    simp [← coe_rpow_of_ne_zero this, NNReal.rpow_add this]

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