add

Mathlib.RingTheory.MvPowerSeries.Evaluation

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.HasEval.add

← MathLib Explorer

English

If a and b have HasEval, then their sum a + b also has HasEval (closure under addition).

Русский

Если a и b имеют HasEval, то и их сумма HasEval.

LaTeX

$$$HasEval(a+b)$$$

Lean4

theorem add [ContinuousAdd S] [IsLinearTopology S S] {a b : σ → S} (ha : HasEval a) (hb : HasEval b) : HasEval (a + b)
    where
  hpow s := (ha.hpow s).add (hb.hpow s)
  tendsto_zero := by rw [← add_zero 0]; exact ha.tendsto_zero.add hb.tendsto_zero

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru