coe_add

Mathlib.Topology.Algebra.GroupCompletion

URI: https://scilib.ai/kg/mathlib#UniformSpace.Completion.coe_add

English

The embedding to Completion α preserves addition: the image of a + b equals the sum of the images.

Русский

Образ a + b в дополнении α равен сумме образов a и b.

LaTeX

$$$\\mathrm{coe}'(a + b) = \\mathrm{coe}'(a) + \\mathrm{coe}'(b)$$$

Lean4

@[norm_cast]
theorem coe_add (a b : α) : ((a + b : α) : Completion α) = a + b :=
  (map₂_coe_coe a b (· + ·) uniformContinuous_add).symm

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

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

Разделы

Аффилиация

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