t3Space

Mathlib.Topology.Separation.Regular

URI: https://scilib.ai/kg/mathlib#T4Space.t3Space

← MathLib Explorer

English

Every T4 space is a T3 space.

Русский

Каждое T4-пространство является T3-пространством.

LaTeX

$$$ [T4Space X] \\Rightarrow [T3Space X]$$$

Lean4

instance (priority := 100) t3Space [T4Space X] : T3Space X where
  regular hs
    hxs := by
    simpa only [nhdsSet_singleton] using
      (normal_separation hs isClosed_singleton (disjoint_singleton_right.mpr hxs)).disjoint_nhdsSet

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

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

Разделы

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

Аффилиация

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