metrizableSpace — Mathlib

English

If f: X → Y is an embedding and Y is metrizable, then X is metrizable.

Русский

Если f: X → Y — вложение и Y метризуемо, то X метризуемо.

LaTeX

$$$\text{IsEmbedding}(f) \Rightarrow [\text{MetrizableSpace } X]$$$

Lean4

/-- Given an embedding of a topological space into a metrizable space, the source space is also
metrizable. -/
theorem _root_.Topology.IsEmbedding.metrizableSpace [MetrizableSpace Y] {f : X → Y} (hf : IsEmbedding f) :
    MetrizableSpace X :=
  letI : MetricSpace Y := metrizableSpaceMetric Y
  ⟨⟨hf.comapMetricSpace f, rfl⟩⟩

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