eq_partialSum' — Mathlib

English

If f and g are equal near x, then CPolynomialAt 𝕜 f x iff CPolynomialAt 𝕜 g x.

Русский

Если f и g совпадают около x, то CPolynomialAt 𝕜 f x эквивалентно CPolynomialAt 𝕜 g x.

LaTeX

$$(f =^\infty_{𝓝 x} g) → (CPolynomialAt 𝕜 f x ↔ CPolynomialAt 𝕜 g x)$$

Lean4

/-- Variant of the previous result with the variable expressed as `y` instead of `x + y`. -/
theorem eq_partialSum' (hf : HasFiniteFPowerSeriesOnBall f p x n r) :
    ∀ y ∈ EMetric.ball x r, ∀ m, n ≤ m → f y = p.partialSum m (y - x) :=
  by
  intro y hy m hm
  rw [EMetric.mem_ball, edist_eq_enorm_sub, ← mem_emetric_ball_zero_iff] at hy
  rw [← (HasFiniteFPowerSeriesOnBall.eq_partialSum hf _ hy m hm), add_sub_cancel]

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