mul — Mathlib

English

Multiplication of analytic functions (valued in a normed algebra) is analytic in a neighborhood.

Русский

Умножение аналитических функций, значения которых лежат в нормированном алгебре, аналитично в окрестности.

LaTeX

$$$\text{AnalyticOnNhd}_{\mathbb{k}}(f,s) \land \text{AnalyticOnNhd}_{\mathbb{k}}(g,s) \Rightarrow \text{AnalyticOnNhd}_{\mathbb{k}}(\lambda x. f(x) \cdot g(x), s)$$$

Lean4

/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
theorem mul {f g : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
    AnalyticOn 𝕜 (fun x ↦ f x * g x) s := fun _ m ↦ (hf _ m).mul (hg _ m)

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