mono — Mathlib

English

If f has a power series at x, and g agrees with f near x, then g has a power series at x with the same radius.

Русский

Если у f есть степенной ряд в точке x, и g совпадает с f near x, то g имеет степенной ряд в точке x с тем же радиусом.

LaTeX

$$$HasFPowerSeriesAt\ f\ p\ x \Rightarrow (f\sim_{nhds(x)} g) \Rightarrow HasFPowerSeriesAt\ g\ p\ x$$$

Lean4

theorem mono (hf : HasFPowerSeriesOnBall f p x r) (r'_pos : 0 < r') (hr : r' ≤ r) : HasFPowerSeriesOnBall f p x r' :=
  ⟨le_trans hr hf.1, r'_pos, fun hy => hf.hasSum (EMetric.ball_subset_ball hr hy)⟩

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