instNoncompactSpaceAdditive

Mathlib.Topology.Constructions

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

English

If X is noncompact, then the additive version Additive X is noncompact.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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