congr — Mathlib

English

If f and g are equal near x, then f has a polynomial expansion at x iff g has one at x.

Русский

Если функции f и g совпадают в окрестности точки x, то существование полиномиального разложения у f в точке x эквивалентно существованию разложения у g в точке x.

LaTeX

$$$(f =^\infty_{𝓝 x} g) \Rightarrow (CPolynomialAt 𝕜 f x \iff CPolynomialAt 𝕜 g x).$$$

Lean4

theorem congr (hf : CPolynomialAt 𝕜 f x) (hg : f =ᶠ[𝓝 x] g) : CPolynomialAt 𝕜 g x :=
  let ⟨_, _, hpf⟩ := hf
  (hpf.congr hg).cpolynomialAt

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