analyticAt_mul — Mathlib

English

The product of two analytic functions, when one is scalar-valued and the other is vector-valued, is analytic jointly in both variables.

Русский

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

LaTeX

$$$\text{AnalyticAt}_{\mathbb{k}}(\lambda x. x_1 \cdot x_2)\,z$$$

Lean4

/-- Multiplication in a normed algebra over `𝕜` is analytic. -/
@[fun_prop]
theorem analyticAt_mul (z : A × A) : AnalyticAt 𝕜 (fun x : A × A ↦ x.1 * x.2) z :=
  (ContinuousLinearMap.mul 𝕜 A).analyticAt_bilinear z

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