instRegularSpaceProd — Mathlib

English

If X and Y are regular spaces, then X × Y with the product topology is regular.

Русский

Если X и Y регулярны, то произведение X × Y с произведной топологией — регулярное пространство.

LaTeX

$$$\text{RegularSpace}(X) \land \text{RegularSpace}(Y) \Rightarrow \text{RegularSpace}(X \times Y)$$$

Lean4

instance [TopologicalSpace Y] [RegularSpace Y] : RegularSpace (X × Y) :=
  (regularSpace_induced (@Prod.fst X Y)).inf (regularSpace_induced (@Prod.snd X Y))

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