toT5Space

Mathlib.Topology.Separation.GDelta

URI: https://scilib.ai/kg/mathlib#T6Space.toT5Space

English

A space that is T6 is also T5.

Русский

Пространство типа T6 также является T5.

LaTeX

$$$ \operatorname{T6Space}(X) \Rightarrow \operatorname{T5Space}(X) $$$

Lean4

/-- A `T₆` space is a `T₅` space. -/
instance (priority := 100) toT5Space [T6Space X] : T5Space X where

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

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

Разделы

Аффилиация

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