instTopologicalSpaceMultiplicative

Mathlib.Topology.Constructions

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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