metrizableSpace

Mathlib.Topology.Metrizable.Uniformity

URI: https://scilib.ai/kg/mathlib#EMetricSpace.metrizableSpace

English

An extended metric space (EMetricSpace) is metrizable.

Русский

Расширенное метрическое пространство метризуемо.

LaTeX

$$$\\text{EMetricSpace}(X) \\Rightarrow \\text{MetrizableSpace}(X)$$$

Lean4

instance (priority := 100) metrizableSpace [EMetricSpace α] : MetrizableSpace α :=
  inferInstance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru