toMetrizableSpace — 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) \land [\text{MetrizableSpace } Y] \Rightarrow [\text{MetrizableSpace } X]$$$

Lean4

instance (priority := 100) toMetrizableSpace [T0Space X] [h : PseudoMetrizableSpace X] : MetrizableSpace X :=
  letI := pseudoMetrizableSpacePseudoMetric X
  ⟨.ofT0PseudoMetricSpace X, rfl⟩

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