discreteUniformity_iff_eq_principal_idRel

English

For any space X with uniformity, the discrete uniformity equals the principalization of idRel; equivalently, DiscreteUniformity X is the same as uniformity X generated by the identity relation.

Русский

Для пространства X с равномерностью дискретная равномерность равна главной величине по отношению idRel; то есть DiscreteUniformity X совпадает с uniformity X, порождаемой отношением равенства.

LaTeX

$$$[\text{UniformSpace } X] \Rightarrow (DiscreteUniformity X) \equiv (uniformity X = \text{principal } idRel)$$$

Lean4

theorem _root_.discreteUniformity_iff_eq_principal_idRel {X : Type*} [UniformSpace X] :
    DiscreteUniformity X ↔ uniformity X = principal idRel := by
  rw [discreteUniformity_iff_eq_bot, UniformSpace.ext_iff, Filter.ext_iff, bot_uniformity]

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