instAdd

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.instAdd

English

There is a natural addition on CauSeq β abv given by pointwise addition: (f+g)(n) = f(n) + g(n).

Русский

Существует естественное сложение CauSeq β abv, заданное покомпонентно: (f+g)(n) = f(n) + g(n).

LaTeX

$$$(f+g)(n) = f(n) + g(n)$$$

Lean4

instance : Add (CauSeq β abv) :=
  ⟨fun f g => ⟨f + g, f.2.add g.2⟩⟩

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

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

Разделы

Аффилиация

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