add — Mathlib

English

The sum p.sum of a formal multilinear series is continuous on its disk of convergence, i.e., continuous on EMetric.ball 0 p.radius.

Русский

Сумма p.sum ряда формальных многосвязей непрерывна на диске сходимости: EMetric.ball 0 p.radius.

LaTeX

$$$ ContinuousOn p.sum (EMetric.ball 0 p.radius) $$$

Lean4

theorem add (hf : HasFiniteFPowerSeriesOnBall f pf x n r) (hg : HasFiniteFPowerSeriesOnBall g pg x m r) :
    HasFiniteFPowerSeriesOnBall (f + g) (pf + pg) x (max n m) r :=
  ⟨hf.1.add hg.1, fun N hN ↦ by
    rw [Pi.add_apply, hf.finite _ ((le_max_left n m).trans hN), hg.finite _ ((le_max_right n m).trans hN), zero_add]⟩

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