smul — Mathlib

English

Coordinate-wise analyticity implies joint analyticity of the vector-valued map.

Русский

Аналитичность по координатам в совокупности приводит к совместной аналитичности векторного отображения.

LaTeX

$$$\text{AnalyticOn}_{\mathbb{k}}(f\!\cdot\!x)\,s \Rightarrow \text{AnalyticOn}_{\mathbb{k}}(\lambda i. f_i, s)$$$

Lean4

/-- Scalar multiplication of one analytic function by another. -/
theorem smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {s : Set E} (hf : AnalyticOn 𝕜 f s)
    (hg : AnalyticOn 𝕜 g s) : AnalyticOn 𝕜 (fun x ↦ f x • g x) s := fun _ m ↦ (hf _ m).smul (hg _ m)

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