fpowerSeriesBilinear_radius — Mathlib

English

The bilinear map (u,v) ↦ f u v is analytic at x, i.e., HasFPowerSeriesAt holds for it.

Русский

Билинейное отображение аналитично в точке x, т.е. выполняется HasFPowerSeriesAt.

LaTeX

$$$ (\text{HasFPowerSeriesAt } (\lambda (u,v) \mapsto f u v) (f.fpowerSeriesBilinear x) x)$$$

Lean4

@[simp]
theorem fpowerSeriesBilinear_radius (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) : (f.fpowerSeriesBilinear x).radius = ∞ :=
  (f.fpowerSeriesBilinear x).radius_eq_top_of_forall_image_add_eq_zero 3 fun _ => rfl

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