continuous_completion

Mathlib.Topology.Algebra.GroupCompletion

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

← MathLib Explorer

English

The composition of the completion extension with continuous smul is continuous.

Русский

Сочетание дополнения и непрерывного скалярного умножения непрерывно.

LaTeX

$$$\\text{Continuous}(\\mathrm{extension})$$$

Lean4

@[continuity]
theorem continuous_completion (f : α →+ β) (hf : Continuous f) :
    Continuous (AddMonoidHom.completion f hf : Completion α → Completion β) :=
  continuous_map

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

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

Разделы

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

Аффилиация

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