congr — Mathlib

English

If f has a finite F-power series on ball and g matches f on that ball, then g also has a finite F-power series on ball.

Русский

Если f имеет конечный F-ряд по шару и g совпадает с f на шаре, то и g имеет конечный F-ряд по шару.

LaTeX

$$HasFiniteFPowerSeriesOnBall f p x n r → EqOn f g (EMetric.ball x r) → HasFiniteFPowerSeriesOnBall g p x n r$$

Lean4

theorem congr (hf : HasFiniteFPowerSeriesOnBall f p x n r) (hg : EqOn f g (EMetric.ball x r)) :
    HasFiniteFPowerSeriesOnBall g p x n r :=
  ⟨hf.1.congr hg, hf.finite⟩

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