instT2Space

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

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

English

If each R_i is T2 (Hausdorff), then the restricted product is T2.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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