exp_add — Mathlib

English

Let x and y be extended real numbers. Then exp(x + y) = exp(x) exp(y).

Русский

Пусть x и y — расширенные вещественные числа. Тогда exp(x + y) = exp(x) exp(y).

LaTeX

$$$\exp(x+y) = \exp x \cdot \exp y$$$

Lean4

theorem exp_add (x y : EReal) : exp (x + y) = exp x * exp y :=
  by
  induction x
  · simp
  · induction y
    · simp
    · simp only [← EReal.coe_add, exp_coe]
      rw [← ENNReal.ofReal_mul (Real.exp_nonneg _), Real.exp_add]
    · simp only [EReal.coe_add_top, exp_top, exp_coe]
      rw [ENNReal.mul_top]
      simp [Real.exp_pos]
  · induction y
    · simp
    · simp only [EReal.top_add_coe, exp_top, exp_coe]
      rw [ENNReal.top_mul]
      simp [Real.exp_pos]
    · simp

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