congr — 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.

Русский

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

LaTeX

$$$HasFPowerSeriesAt\ f p x \Rightarrow (g =\!\!\!\! _{nhds(x)} f) \Rightarrow HasFPowerSeriesAt\ g p x$$$

Lean4

theorem congr (hf : HasFPowerSeriesAt f p x) (hg : f =ᶠ[𝓝 x] g) : HasFPowerSeriesAt g p x :=
  by
  rcases hf with ⟨r₁, h₁⟩
  rcases EMetric.mem_nhds_iff.mp hg with ⟨r₂, h₂pos, h₂⟩
  exact
    ⟨min r₁ r₂,
      (h₁.mono (lt_min h₁.r_pos h₂pos) inf_le_left).congr fun y hy => h₂ (EMetric.ball_subset_ball inf_le_right hy)⟩

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