discreteTopology_of_discrete_uniformity

English

If a uniform space α has the discrete uniformity, then α carries the discrete topology.

Русский

Если равномерность пространства α является дискретной, то топология α дискретна.

LaTeX

$$$$\mathcal{U}(\\alpha) = \\mathcal{P}(\\mathrm{idRel}) \\implies \\mathrm{DiscreteTopology}(\\alpha).$$$$

Lean4

/-- A uniform space with the discrete uniformity has the discrete topology. -/
theorem discreteTopology_of_discrete_uniformity [hα : UniformSpace α] (h : uniformity α = 𝓟 idRel) :
    DiscreteTopology α :=
  ⟨(UniformSpace.ext h.symm : ⊥ = hα) ▸ rfl⟩

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