mul — Mathlib

English

The pointwise product of analytic functions is analytic on a set.

Русский

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

LaTeX

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

Lean4

/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/
@[fun_prop]
theorem mul {f g : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (hg : AnalyticAt 𝕜 g z) : AnalyticAt 𝕜 (f * g) z :=
  hf.fun_mul hg

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