coe_sub

Mathlib.Topology.Algebra.GroupCompletion

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

English

The embedding to Completion α preserves subtraction: the image of a − b equals the difference of the images.

Русский

Образ a − b в дополнении α равен разности образов a и b.

LaTeX

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

Lean4

@[norm_cast]
theorem coe_sub (a b : α) : ((a - b : α) : Completion α) = a - b :=
  (map₂_coe_coe a b Sub.sub uniformContinuous_sub).symm

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

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

Разделы

Аффилиация

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