instParacompactSpaceProdOfCompactSpace_1

Mathlib.Topology.Compactness.Paracompact

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

← MathLib Explorer

English

If X is paracompact and Y is compact, then X × Y is paracompact.

Русский

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

LaTeX

$$$ \\text{ParacompactSpace}(X \\times Y) $$$

Lean4

instance (priority := 200) [ParacompactSpace X] [CompactSpace Y] : ParacompactSpace (X × Y) :=
  (Homeomorph.prodComm X Y).paracompactSpace_iff.2 inferInstance

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

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

Разделы

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

Аффилиация

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