English
The pointwise product of two analytic functions is analytic on a set, provided each is analytic on that set.
Русский
Поточечное произведение двух аналитических функций аналитично на множестве, если каждая аналитична на этом множестве.
LaTeX
$$$\text{AnalyticOn}_{\mathbb{k}}(f,s) \land \text{AnalyticOn}_{\mathbb{k}}(g,s) \Rightarrow \text{AnalyticOn}_{\mathbb{k}}(\lambda x. f(x) \cdot g(x), s)$$$
Lean4
/-- Scalar multiplication of one analytic function by another. -/
@[fun_prop]
theorem fun_smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E} (hf : AnalyticAt 𝕜 f z)
(hg : AnalyticAt 𝕜 g z) : AnalyticAt 𝕜 (fun x ↦ f x • g x) z :=
(analyticAt_smul _).comp₂ hf hg
