instDiscreteTopologyOfAlexandrovDiscreteOfT1Space

Mathlib.Topology.Separation.AlexandrovDiscrete

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

← MathLib Explorer

English

If X is Alexandrov-discrete and T1, then X has the discrete topology.

Русский

Если X Alexandrov-discrete и T1, то топология X дискретна.

LaTeX

$$DiscreteTopology X$$

Lean4

instance (priority := low) [AlexandrovDiscrete X] [T1Space X] : DiscreteTopology X := by
  simp [discreteTopology_iff_nhds, ← principal_nhdsKer_singleton]

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

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

Разделы

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

Аффилиация

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