hasFPowerSeriesAt_bilinear — Mathlib

English

The bilinear map x ↦ f x.1 x.2 has HasFPowerSeriesAt with the bilinear fpowerSeriesBilinear as its expansion.

Русский

Билинейное отображение x ↦ f x.1 x.2 имеет HasFPowerSeriesAt с expansion через fpowerSeriesBilinear.

LaTeX

$$$ HasFPowerSeriesAt (\lambda x => f x.1 x.2) (f.fpowerSeriesBilinear x) x $$$

Lean4

protected theorem hasFPowerSeriesAt_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    HasFPowerSeriesAt (fun x : E × F => f x.1 x.2) (f.fpowerSeriesBilinear x) x :=
  ⟨∞, f.hasFPowerSeriesOnBall_bilinear x⟩

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