instRegularSpaceForall — Mathlib

English

If each X_i is a regular space, then the space of all functions i ↦ X_i (with the appropriate product topology) is regular.

Русский

Если каждое X_i — регулярное пространство, то пространство функций i ↦ X_i регулярно.

LaTeX

$$$\forall i, RegularSpace(X_i) \Rightarrow RegularSpace((i : I) \to X_i)$$$

Lean4

instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, RegularSpace (X i)] :
    RegularSpace (∀ i, X i) :=
  regularSpace_iInf fun _ => regularSpace_induced _

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