completelyRegularSpace_induced — Mathlib

English

If X and Y are completely regular, then their product X × Y is completely regular.

Русский

Произведение двух полностью регулярных пространств полностью регулярно.

LaTeX

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

Lean4

theorem completelyRegularSpace_induced {X Y : Type*} {t : TopologicalSpace Y} (ht : @CompletelyRegularSpace Y t)
    (f : X → Y) : @CompletelyRegularSpace X (t.induced f) :=
  @IsInducing.completelyRegularSpace _ (t.induced f) _ t _ _ (IsInducing.induced f)

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