instNoncompactSpaceMultiplicative

Mathlib.Topology.Constructions

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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