instT35SpaceProd

Mathlib.Topology.Separation.CompletelyRegular

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

English

An instance of the previous: a product of CR spaces is CR.

Русский

Порождающее свойство: произведение CR-пространств — CR.

LaTeX

$$$[instCompletelyRegularSpaceForall]$$$

Lean4

instance {X Y : Type*} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [htX : T35Space X] [htY : T35Space Y] :
    T35Space (X × Y) where

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

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

Разделы

Аффилиация

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