instMetrizableSpace

Mathlib.Topology.Metrizable.ContinuousMap

URI: https://scilib.ai/kg/mathlib#ContinuousMap.instMetrizableSpace

English

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

Русский

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

LaTeX

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

Lean4

instance [MetrizableSpace Y] : MetrizableSpace C(X, Y) :=
  let _ := metrizableSpaceMetric Y
  UniformSpace.metrizableSpace

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

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

Разделы

Аффилиация

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