toPseudoMetrizableSpace

Mathlib.Topology.Metrizable.Basic

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace

← MathLib Explorer

English

If X is pseudo-metrizable and T0, then X is metrizable.

Русский

Если X псевдометризуемо и T0, тогда X метризуемо.

LaTeX

$$$[\text{T0Space } X] \land [\text{PseudoMetrizableSpace } X] \Rightarrow [\text{MetrizableSpace } X]$$$

Lean4

instance (priority := 100) toPseudoMetrizableSpace [h : MetrizableSpace X] : PseudoMetrizableSpace X :=
  let ⟨m, hm⟩ := h.1
  ⟨⟨m.toPseudoMetricSpace, hm⟩⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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