fpowerSeries_radius — Mathlib

English

For a continuous linear map f, the radius of its power series at any x is infinite: (f.fpowerSeries x).radius = ∞.

Русский

Для непрерывного линейного отображения f радиус его степенного ряда в любой точке x равен бесконечности: (f.fpowerSeries x).radius = ∞.

LaTeX

$$$\left( f.fpowerSeries x \right).radius = \infty$$$

Lean4

@[simp]
theorem fpowerSeries_radius (f : E →L[𝕜] F) (x : E) : (f.fpowerSeries x).radius = ∞ :=
  (f.fpowerSeries x).radius_eq_top_of_forall_image_add_eq_zero 2 fun _ => rfl

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