English
If f and g agree in a neighborhood of x, then having a polynomial expansion at x for f is equivalent to having one for g; i.e., CPolynomialAt 𝕜 f x holds iff CPolynomialAt 𝕜 g x holds whenever f and g coincide near x.
Русский
Если функции f и g совпадают в окрестности точки x, то существование полиномиального разложения у f в точке x эквивалентно существованию такого разложения у g; то есть CPolynomialAt 𝕜 f x равно CPolynomialAt 𝕜 g x, когда f и g совпадают около x.
LaTeX
$$$(f =^\infty_{n x} g) \Rightarrow (CPolynomialAt\ 𝕜\ f\ x \iff CPolynomialAt\ 𝕜\ g\ x).$$$
Lean4
theorem congr (hf : HasFiniteFPowerSeriesAt f p x n) (hg : f =ᶠ[𝓝 x] g) : HasFiniteFPowerSeriesAt g p x n :=
Exists.imp (fun _ hg ↦ ⟨hg, hf.finite⟩) (hf.hasFPowerSeriesAt.congr hg)
