pseudoMetrizableSpacePseudoMetric

English

If a space X is pseudo-metrizable, there exists a pseudometric d on X whose topology agrees with the given one, i.e. τ(d) = τ.

Русский

Если X псевдометризуема, существует псевдометрическое расстояние d на X, такое что топология, порождённая d, совпадает с данной топологией.

LaTeX

$$$\exists d: X \times X \to \mathbb{R}_{\ge 0},\; \text{PseudoMetric}(d)\text{ and } \tau(d)=\tau$$$

Lean4

/-- Construct on a metrizable space a metric compatible with the topology. -/
noncomputable def pseudoMetrizableSpacePseudoMetric (X : Type*) [TopologicalSpace X] [h : PseudoMetrizableSpace X] :
    PseudoMetricSpace X :=
  h.exists_pseudo_metric.choose.replaceTopology h.exists_pseudo_metric.choose_spec.symm

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