instT35SpaceSubtype

Mathlib.Topology.Separation.CompletelyRegular

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

English

CR on a space transfers to subtypes via IsInducing subtypeVal.

Русский

CR на пространстве передается к подпространствам через отображение subtypeVal.

LaTeX

$$$[instCompletelyRegularSpaceSubtype]$$$

Lean4

instance {p : X → Prop} [T35Space X] : T35Space (Subtype p) where

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

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

Разделы

Аффилиация

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