English
If X closed-embeds into a completely metrizable space Y, then X is completely metrizable.
Русский
Если отображение X в Y является замыканием и вложением, и Y полностью метризуемо, то X тоже метризуема.
LaTeX
$$$\\forall X Y, [TopologicalSpace X] [TopologicalSpace Y] [IsCompletelyMetrizableSpace Y] {f : X \\to Y} (hf : IsClosedEmbedding f)\\Rightarrow IsCompletelyMetrizableSpace X$$$
Lean4
/-- Given a closed embedding into a completely metrizable space,
the source space is also completely metrizable. -/
theorem _root_.Topology.IsClosedEmbedding.IsCompletelyMetrizableSpace [TopologicalSpace X] [TopologicalSpace Y]
[IsCompletelyMetrizableSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) : IsCompletelyMetrizableSpace X :=
by
letI := upgradeIsCompletelyMetrizable Y
letI : MetricSpace X := hf.isEmbedding.comapMetricSpace f
have : CompleteSpace X :=
by
rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]
exact hf.isClosed_range.isComplete
infer_instance
