instAddCauchy

Mathlib.Algebra.Order.CauSeq.Completion

URI: https://scilib.ai/kg/mathlib#CauSeq.Completion.instAddCauchy

English

Addition on the completion is induced by addition on Cauchy sequences: mk f + mk g = mk (f + g).

Русский

Сложение в завершении определяется покомпонентно: mk f + mk g = mk (f + g).

LaTeX

$$$mk\,f + mk\,g = mk\,(f + g)$$$

Lean4

instance : Add (Cauchy abv) :=
  ⟨(Quotient.map₂ (· + ·)) fun _ _ hf _ _ hg => add_equiv_add hf hg⟩

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

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

Разделы

Аффилиация

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