upgradeIsCompletelyMetrizable — Mathlib

English

This construction equips a completely metrizable space with a complete metric. It can be used to obtain a canonical upgraded metrizable structure.

Русский

Данная конструкция наделяет полностью метризуемое пространство полной метрикой, образуя каноническую обновлённую метрическую структуру.

LaTeX

$$$\\text{upgradeIsCompletelyMetrizable}(X)\\text{ yields an } UpgradedIsCompletelyMetrizableSpace X\\text{ with a distinguished complete metric.}$$$

Lean4

/-- This definition endows a completely metrizable space with a complete metric. Use it as:
`letI := upgradeIsCompletelyMetrizable X`. -/
noncomputable def upgradeIsCompletelyMetrizable (X : Type*) [TopologicalSpace X] [IsCompletelyMetrizableSpace X] :
    UpgradedIsCompletelyMetrizableSpace X :=
  letI := completelyMetrizableMetric X
  { complete_completelyMetrizableMetric X with }

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