metrizableSpace — Mathlib

English

A T0 uniform space with countably generated 𝓤 X is metrizable.

Русский

Унитное пространство с счетной порождаемостью 𝓤 X метризуемо.

LaTeX

$$$[UniformSpace X] [IsCountablyGenerated (\\mathcal U X)] [T0Space X]\\Rightarrow TopologicalSpace.MetrizableSpace X$$$

Lean4

/-- A T₀ uniform space with countably generated `𝓤 X` is metrizable. This is not an instance to
avoid loops. -/
theorem metrizableSpace [UniformSpace X] [IsCountablyGenerated (𝓤 X)] [T0Space X] :
    TopologicalSpace.MetrizableSpace X := by
  letI := UniformSpace.metricSpace X
  infer_instance

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