toT4Space

Mathlib.Topology.Separation.Regular

URI: https://scilib.ai/kg/mathlib#T5Space.toT4Space

English

A T5 space is a T4 space.

Русский

T5-пространство является T4-пространством.

LaTeX

$$$ [T5Space X] \\Rightarrow [T4Space X]$$$

Lean4

/-- A `T₅` space is a `T₄` space. -/
instance (priority := 100) toT4Space [T5Space X] : T4Space X where
  -- follows from type-class inference

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

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

Разделы

Аффилиация

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