smul — Mathlib

English

If f and g are analytic at a point z, then the product x ↦ f(x) • g(x) is analytic at z.

Русский

Если f и g аналитичны в точке z, то произведение x ↦ f(x)•g(x) аналитично в z.

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

/-- Scalar multiplication of one analytic function by another. -/
@[fun_prop]
theorem smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E} (hf : AnalyticAt 𝕜 f z)
    (hg : AnalyticAt 𝕜 g z) : AnalyticAt 𝕜 (f • g) z :=
  hf.fun_smul hg

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