rexp — Mathlib

English

If f has sum a, then exp ∘ f has product exp(a). In other words, the infinite product of exp(f(i)) equals exp of the sum a.

Русский

Если f имеет сумму a, то exp ∘ f имеет произведение exp(a). Иными словами, бесконечное произведение exp(f(i)) равно exp суммы a.

LaTeX

$$$ \text{HasSum } f a \Rightarrow \text{HasProd } (\exp \circ f) (\exp a) $$$

Lean4

/-- If `f` has sum `a`, then `exp ∘ f` has product `exp a`. -/
theorem «rexp» {ι} {f : ι → ℝ} {a : ℝ} (h : HasSum f a) : HasProd (rexp ∘ f) (rexp a) :=
  Tendsto.congr (fun s ↦ exp_sum s f) <| Tendsto.rexp h

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