denseRange_toCompl

Mathlib.Analysis.Normed.Group.HomCompletion

URI: https://scilib.ai/kg/mathlib#NormedAddCommGroup.denseRange_toCompl

English

The map toCompl has dense range in the completion space.

Русский

Образ toCompl плотный в пространстве завершения.

LaTeX

$$$ DenseRange( toCompl : G \to \mathrm{Completion} G ).$$$

Lean4

theorem denseRange_toCompl : DenseRange (toCompl : G → Completion G) :=
  Completion.isDenseInducing_coe.dense

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

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

Разделы

Аффилиация

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