completion_coe

Mathlib.Topology.Algebra.GroupCompletion

URI: https://scilib.ai/kg/mathlib#AddMonoidHom.completion_coe

← MathLib Explorer

English

The completion of a sum of two homomorphisms equals the sum of their completions.

Русский

Дополнение суммы двух гомоморфизмов равно сумме их дополнений.

LaTeX

$$$ (f + g).completion (hf hg) = f.completion hf + g.completion hg $$$

Lean4

theorem completion_coe (f : α →+ β) (hf : Continuous f) (a : α) : AddMonoidHom.completion f hf a = f a :=
  map_coe (uniformContinuous_addMonoidHom_of_continuous hf) a

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

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

Разделы

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

Аффилиация

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