sub — Mathlib

English

From hf and hg, deduce HasFPowerSeriesWithinOnBall for f−g with pf−pg.

Русский

Из hf и hg следует HasFPowerSeriesWithinOnBall для f−g с pf−pg.

LaTeX

$$$HasFPowerSeriesWithinOnBall(f pf s x r) \\land HasFPowerSeriesWithinOnBall(g pg s x r) \\Rightarrow HasFPowerSeriesWithinOnBall(f - g, pf - pg, s, x, r)$$$

Lean4

theorem sub (hf : HasFPowerSeriesWithinOnBall f pf s x r) (hg : HasFPowerSeriesWithinOnBall g pg s x r) :
    HasFPowerSeriesWithinOnBall (f - g) (pf - pg) s x r := by simpa only [sub_eq_add_neg] using hf.add hg.neg

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