instTopologicalSpaceAdditive

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#instTopologicalSpaceAdditive

English

The additive construction on a space X carries the same topology as X itself.

Русский

Классическая топология пространства X переносится на структуру Additive X без изменений.

LaTeX

$$$\\operatorname{TopologicalSpace}(\\operatorname{Additive}(X)) = \\operatorname{TopologicalSpace}(X)$$$

Lean4

instance : TopologicalSpace (Additive X) :=
  ‹TopologicalSpace X›

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

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

Разделы

Аффилиация

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