noncompactSpace_right

Mathlib.Topology.Compactness.Compact

URI: https://scilib.ai/kg/mathlib#Prod.noncompactSpace_right

← MathLib Explorer

English

If X is nonempty and Y is noncompact, then X × Y is noncompact.

Русский

Если X непусто и Y некомпактно, то X × Y некомпактно.

LaTeX

$$$\text{Nonempty}(X) \land \text{NoncompactSpace}(Y) \Rightarrow \text{NoncompactSpace}(X \times Y)$$$

Lean4

instance (priority := 100) noncompactSpace_right [Nonempty X] [NoncompactSpace Y] : NoncompactSpace (X × Y) :=
  Prod.noncompactSpace_iff.2 (Or.inr ⟨‹_›, ‹_›⟩)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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