discreteUniformity_iff_idRel_mem_uniformity

English

In a space X with uniformity, the relation idRel belongs to the uniformity of X.

Русский

В пространстве X с равномерностью отношение idRel принадлежит равномерности пространства.

LaTeX

$$$idRel \in uniformity(X)$$$

Lean4

theorem _root_.discreteUniformity_iff_idRel_mem_uniformity {X : Type*} [UniformSpace X] :
    DiscreteUniformity X ↔ idRel ∈ uniformity X := by rw [← uniformSpace_eq_bot, discreteUniformity_iff_eq_bot]

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