instT3Space

Mathlib.Topology.Separation.Regular

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

English

If X is T0 and Regular, then X is T3-space.

Русский

Если пространство X удовлетворяет условиям T0 и Regular, то оно является T3-пространством.

LaTeX

$$$[T0Space X] \land [RegularSpace X] \Rightarrow [T3Space X].$$$

Lean4

instance (priority := 90) instT3Space [T0Space X] [RegularSpace X] : T3Space X :=
  ⟨⟩

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

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

Разделы

Аффилиация

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