of_completeSpace_metrizable — Mathlib

English

Let X be a type endowed with a UniformSpace structure. If X is complete as a uniform space, its uniformity is countably generated, and X is T0, then the underlying topological space is completely metrizable.

Русский

Пусть X — множество с равномерным пространством. Если X является полным как равномерное пространство, его равномерность счетно порождается и X является T0, тогда исходное топологическое пространство счетно метризуемо (совершенно метризируемо).

LaTeX

$$$\\forall X,\\ [\\text{UniformSpace } X]\\ \\land\\ [\\text{CompleteSpace } X]\\ \\land\\ [(\\mathcal U X).IsCountablyGenerated]\\ \\land\\ [T_0Space X]\\Rightarrow IsCompletelyMetrizableSpace X$$$

Lean4

instance (priority := 100) of_completeSpace_metrizable [UniformSpace X] [CompleteSpace X] [(𝓤 X).IsCountablyGenerated]
    [T0Space X] : IsCompletelyMetrizableSpace X where complete := ⟨UniformSpace.metricSpace X, rfl, ‹_›⟩

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