English
If f and g are analytic within a set s at z, then the product x ↦ f(x) • g(x) is analytic within s at z.
Русский
Если f и g аналитичны внутри множества s в z, то отображение x ↦ f(x)•g(x) аналитично внутри s в z.
LaTeX
$$$\text{AnalyticWithinAt}_{\mathbb{k}}(f,s,z) \land \text{AnalyticWithinAt}_{\mathbb{k}}(g,s,z) \Rightarrow \text{AnalyticWithinAt}_{\mathbb{k}}(\lambda x. f(x) \cdot g(x), s, z)$$$
Lean4
/-- Scalar multiplication of one analytic function by another. -/
theorem smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {s : Set E} {z : E}
(hf : AnalyticWithinAt 𝕜 f s z) (hg : AnalyticWithinAt 𝕜 g s z) : AnalyticWithinAt 𝕜 (fun x ↦ f x • g x) s z :=
(analyticAt_smul _).comp₂_analyticWithinAt hf hg
