rpow_add_of_nonneg — Mathlib

English

If x ≠ ∞ and y+z is real, x^(y+z) = x^y · x^z when applicable.

Русский

Если x ≠ ∞ и y+z реально, тогда x^(y+z) = x^y · x^z при условии применимости.

LaTeX

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

Lean4

theorem rpow_add_of_nonneg {x : ℝ≥0∞} (y z : ℝ) (hy : 0 ≤ y) (hz : 0 ≤ z) : x ^ (y + z) = x ^ y * x ^ z :=
  by
  induction x using recTopCoe
  · rcases hy.eq_or_lt with rfl | hy
    · rw [rpow_zero, one_mul, zero_add]
    rcases hz.eq_or_lt with rfl | hz
    · rw [rpow_zero, mul_one, add_zero]
    simp [top_rpow_of_pos, hy, hz, add_pos hy hz]
  simp [← coe_rpow_of_nonneg, hy, hz, add_nonneg hy hz, NNReal.rpow_add_of_nonneg _ hy hz]

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