t3Space_iff_t0Space

Mathlib.Topology.Separation.Regular

URI: https://scilib.ai/kg/mathlib#RegularSpace.t3Space_iff_t0Space

← MathLib Explorer

English

In a RegularSpace, T3Space is equivalent to T0Space.

Русский

В регулярном пространстве T3 эквивалентно T0.

LaTeX

$$$[RegularSpace X] \Rightarrow (T3Space X \iff T0Space X).$$$

Lean4

theorem t3Space_iff_t0Space [RegularSpace X] : T3Space X ↔ T0Space X := by
  constructor <;> intro <;>
    infer_instance
      -- see Note [lower instance priority]

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

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

Разделы

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

Аффилиация

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