restrictScalars — Mathlib

English

Restriction of scalars preserves HasFPowerSeriesWithinOnBall: a power series within on a ball remains valid after restricting scalars.

Русский

Сужение скаляров сохраняет HasFPowerSeriesWithinOnBall: степенной ряд в шаре сохраняется после ограничения скаляров.

LaTeX

$$$\text{HasFPowerSeriesWithinOnBall}(f,p,s,x,r) \Rightarrow \text{HasFPowerSeriesWithinOnBall}(f,p\!\restrictionScalars\;\mathbb{K},s,x,r)$$$

Lean4

theorem restrictScalars (hf : HasFPowerSeriesWithinOnBall f p s x r) :
    HasFPowerSeriesWithinOnBall f (p.restrictScalars 𝕜) s x r :=
  ⟨hf.r_le.trans (FormalMultilinearSeries.radius_le_of_le (fun n ↦ by simp)), hf.r_pos, hf.hasSum⟩

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