t2Space_of_metrizableSpace — Mathlib

English

The construction metrizableSpaceMetric on a metrizable space yields a metric space structure.

Русский

Построение metrizableSpaceMetric на метризуемом пространстве даёт метрическое пространство.

LaTeX

$$$\text{metrizableSpaceMetric}(X) \text{ defines a MetricSpace on } X$$$

Lean4

instance (priority := 100) t2Space_of_metrizableSpace [MetrizableSpace X] : T2Space X :=
  letI : MetricSpace X := metrizableSpaceMetric X
  inferInstance

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