MetrizableSpace — Mathlib

English

If a space X is completely metrizable, then it is metrizable.

Русский

Если пространство X полностью метризуемо, то оно метризируемо.

LaTeX

$$$\\forall X\\, [\\text{TopologicalSpace } X]\\ [IsCompletelyMetrizableSpace X]\\Rightarrow TopologicalSpace.MetrizableSpace X$$$

Lean4

/-- Note: the priority is set to 90 to ensure that this instance is only applied after
`EMetricSpace.metrizableSpace`. This prevents unnecessary attempts to infer completeness. -/
instance (priority := 90) MetrizableSpace [TopologicalSpace X] [IsCompletelyMetrizableSpace X] : MetrizableSpace X :=
  by
  letI := upgradeIsCompletelyMetrizable X
  infer_instance

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