rpow_add_of_nonneg — Mathlib

English

Let x, y, z be real numbers with x ≥ 0, y ≥ 0, z ≥ 0. Then x^(y+z) = x^y · x^z.

Русский

Пусть x, y, z — действительные числа с x ≥ 0, y ≥ 0 и z ≥ 0. Тогда x^(y+z) = x^y · x^z.

LaTeX

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

Lean4

theorem rpow_add_of_nonneg (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) : x ^ (y + z) = x ^ y * x ^ z :=
  by
  rcases hy.eq_or_lt with (rfl | hy)
  · rw [zero_add, rpow_zero, one_mul]
  exact rpow_add' hx (ne_of_gt <| add_pos_of_pos_of_nonneg hy hz)

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