mul — Mathlib

English

Multiplication of analytic functions within a set is analytic.

Русский

Умножение аналитических функций внутри множества сохраняет аналитичность.

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

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

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