instJacobsonSpaceOfT1Space

Mathlib.Topology.JacobsonSpace

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

English

If X is a T1 space, then X is Jacobson.

Русский

Если X — пространство T1, то X является пространством Якобсона.

LaTeX

$$$ \operatorname{T1Space}(X) \Rightarrow \operatorname{JacobsonSpace}(X) $$$

Lean4

instance (priority := 100) [T1Space X] : JacobsonSpace X :=
  ⟨by simp [closedPoints_eq_univ, closure_eq_iff_isClosed]⟩

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

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

Разделы

Аффилиация

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