comp_sub — Mathlib

English

If f has a power series within ball around x with radius r, then the translated function z↦f(z−y) has the same power series p about x+y on s+{y}.

Русский

Если f обладает рядом внутри окружности вокруг x, радиуса r, то z↦f(z−y) имеет тот же ряд p вокруг x+y на множестве s+{y}.

LaTeX

$$$HasFPowerSeriesWithinOnBall\ f\ p\ s\ x\ r \Rightarrow HasFPowerSeriesWithinOnBall\ (\\fun z \\to f (z - y))\ p\ (s + { y })\ (x + y)\ r$$$

Lean4

theorem comp_sub (hf : HasFPowerSeriesWithinAt f p s x) (y : E) :
    HasFPowerSeriesWithinAt (fun z ↦ f (z - y)) p (s + { y }) (x + y) :=
  by
  obtain ⟨r, hf⟩ := hf
  exact ⟨r, hf.comp_sub _⟩

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