instT35SpaceForall

Mathlib.Topology.Separation.CompletelyRegular

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

English

If each X_i in a family is CR, then their product is CR.

Русский

Если каждый X_i в семействе CR, то их произведение CR.

LaTeX

$$$[\\forall i, [CompletelyRegularSpace (X i)]] \\Rightarrow [CompletelyRegularSpace (\\Pi i, X i)]$$$

Lean4

instance {ι : Type*} {X : ι → Type*} [t : Π (i : ι), TopologicalSpace (X i)] [ht : Π (i : ι), T35Space (X i)] :
    T35Space (Π i, X i) where

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

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

Разделы

Аффилиация

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