instUCompactlyGeneratedSpaceOfDiscreteTopology

Mathlib.Topology.Compactness.CompactlyGeneratedSpace

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

← MathLib Explorer

English

If X has a discrete topology, then X is UCompactlyGeneratedSpace.

Русский

Если у X дискретная топология, то X — UCompactlyGeneratedSpace.

LaTeX

$$$ [\text{DiscreteTopology}(X)] \Rightarrow UCompactlyGeneratedSpace(X) $$$

Lean4

instance (X : Type v) [t : TopologicalSpace X] [DiscreteTopology X] : UCompactlyGeneratedSpace.{u} X where
  le_compactlyGenerated := by
    rw [DiscreteTopology.eq_bot (t := t)]
    exact bot_le

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

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

Разделы

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

Аффилиация

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