instT0Space — Mathlib

English

If each R_i is a T0 space, then the restricted product is T0.

Русский

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

LaTeX

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

Lean4

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

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