instT1Space

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

URI: https://scilib.ai/kg/mathlib#RestrictedProduct.instT1Space

English

If each R_i is T1, then the restricted product is T1.

Русский

Если каждый R_i является T1, то ограниченное произведение также T1.

LaTeX

$$$[\\forall i,\\; T_1(R_i)] \\Rightarrow T_1(\\prod^\\mathrm{r}_i [R_i, A_i]_{\\mathcal F}).$$$

Lean4

instance [∀ i, T1Space (R i)] : T1Space (Πʳ i, [R i, A i]_[𝓕]) :=
  t1Space_of_injective_of_continuous DFunLike.coe_injective continuous_coe

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

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

Разделы

Аффилиация

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