instCompletelyRegularSpaceSubtype

English

If Y is completely regular and f: X → Y, then X with the induced topology is completely regular.

Русский

Если Y полностью регулярное и задан отображение f: X → Y, то X с индуцированной топологией полностью регулярно.

LaTeX

$$$[CompletelyRegularSpace Y] \\rightarrow [CompletelyRegularSpace X]\\text{ for }(tind f)$$$

Lean4

instance {p : X → Prop} [CompletelyRegularSpace X] : CompletelyRegularSpace (Subtype p) :=
  Topology.IsInducing.subtypeVal.completelyRegularSpace

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