to_quasiSeparatedSpace

Mathlib.Topology.QuasiSeparated

URI: https://scilib.ai/kg/mathlib#NoetherianSpace.to_quasiSeparatedSpace

English

Every T2 (Hausdorff) space is quasi-separated.

Русский

Каждое пространство Хаусдорфа является квазиразделимым.

LaTeX

$$[T2Space α] ⇒ QuasiSeparatedSpace α$$

Lean4

instance (priority := 100) to_quasiSeparatedSpace [NoetherianSpace α] : QuasiSeparatedSpace α :=
  ⟨fun _ _ _ _ _ _ => NoetherianSpace.isCompact _⟩

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

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

Разделы

Аффилиация

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