instCompactSpaceMultiplicative

Mathlib.Topology.Constructions

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

English

If X is compact, then the multiplicative version Multiplicative X is compact.

Русский

Если X компактно, то Multiplicative X компактно.

LaTeX

$$$\operatorname{CompactSpace}(X) \implies \operatorname{CompactSpace}(\mathrm{Multiplicative}\,X)$$$

Lean4

instance [CompactSpace X] : CompactSpace (Multiplicative X) :=
  ‹CompactSpace X›

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

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

Разделы

Аффилиация

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