instCompletelyRegularSpaceProd — Mathlib

English

If X and Y are CR spaces, then their product X × Y is CR.

Русский

Если X и Y — CR-пространства, то их произведение CR.

LaTeX

$$$[CompletelyRegularSpace X] \\land [CompletelyRegularSpace Y] \\Rightarrow [CompletelyRegularSpace (X \\times Y)]$$$

Lean4

instance {X Y : Type*} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [htX : CompletelyRegularSpace X]
    [htY : CompletelyRegularSpace Y] : CompletelyRegularSpace (X × Y) :=
  completelyRegularSpace_inf (completelyRegularSpace_induced htX _) ((completelyRegularSpace_induced htY _))

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