analyticAt_bilinear — Mathlib

English

The function (u,v) ↦ f u v is analytic in the product space; HasFPowerSeriesAt holds with the bilinear expansion.

Русский

Функция (u,v) ↦ f u v аналитична в произведённом пространстве; HasFPowerSeriesAt действует для билинейного разложения.

LaTeX

$$$ AnalyticAt 𝕜 (\lambda (u,v) => f u v) (x) $$$

Lean4

protected theorem analyticAt_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    AnalyticAt 𝕜 (fun x : E × F => f x.1 x.2) x :=
  (f.hasFPowerSeriesAt_bilinear x).analyticAt

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