fun_mul — Mathlib

English

The product of two analytic functions is analytic at a point.

Русский

Произведение аналитических функций аналитично в точке.

LaTeX

$$$\text{AnalyticAt}_{\mathbb{k}}(f,z) \land \text{AnalyticAt}_{\mathbb{k}}(g,z) \Rightarrow \text{AnalyticAt}_{\mathbb{k}}(\lambda x. f(x) \cdot g(x), z)$$$

Lean4

/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
@[fun_prop]
theorem fun_mul {f g : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) :
    AnalyticAt 𝕜 (fun x ↦ f x * g x) z :=
  (analyticAt_mul _).comp₂ hf hg

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