exp — Mathlib

English

If a sequence f has sum a in a real/complex-valued setting, then exp ∘ f has product exp(a).

Русский

Если сумма функции f равна a, то произведение экспоненты exp ∘ f равно exp(a).

LaTeX

$$$$ \text{If } \text{HasSum } f a, \text{ then } \text{HasProd}(\exp \circ f) (\exp a). $$$$

Lean4

/-- If `f` has sum `a`, then `NormedSpace.exp ∘ f` has product `NormedSpace.exp a`. -/
theorem exp {ι : Type*} {f : ι → 𝔸} {a : 𝔸} (h : HasSum f a) : HasProd (exp 𝕂 ∘ f) (exp 𝕂 a) :=
  Tendsto.congr (fun s ↦ exp_sum s f) <| Tendsto.exp h

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