comp_sub — Mathlib

English

If f has a power series at x, then the translated function z ↦ f(z−y) has a power series p at x+y.

Русский

Если у f есть степенной разложение в точке x, то функция z↦f(z−y) имеет такое же разложение в точке x+y.

LaTeX

$$$HasFPowerSeriesAt\ f\ p\ x \Rightarrow HasFPowerSeriesAt\ (\\fun z \\to f (z - y))\ p\ (x + y)$$$

Lean4

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

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