smul — Mathlib

English

Near-analytic property coordinatewise.

Русский

Ближняя аналитичность по координатам.

LaTeX

$$$\text{AnalyticOnNhd}_{\mathbb{k}}(\lambda x. (f \cdot x))\,s \iff \forall i, \text{AnalyticOnNhd}_{\mathbb{k}}(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 : AnalyticOnNhd 𝕜 f s)
    (hg : AnalyticOnNhd 𝕜 g s) : AnalyticOnNhd 𝕜 (fun x ↦ f x • g x) s := fun _ m ↦ (hf _ m).smul (hg _ m)

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