mul — Mathlib

English

The product of two analytic functions is analytic within a set.

Русский

Произведение аналитических функций аналитично внутри множества.

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} {z : E} (hf : AnalyticWithinAt 𝕜 f s z) (hg : AnalyticWithinAt 𝕜 g s z) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x * g x) s z :=
  (analyticAt_mul _).comp₂_analyticWithinAt hf hg

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