eq_principal_idRel — Mathlib

English

In a uniform space X, the equality between uniformity and the principal filter generated by idRel holds; i.e., uniformity X = principal idRel.

Русский

В равномерном пространстве X выполняется равенство: равномерность X равна главному фильтру, порождаемому idRel.

LaTeX

$$$uniformity(X) = \text{principal } idRel$$$

Lean4

theorem eq_principal_idRel : uniformity X = principal idRel :=
  discreteUniformity_iff_eq_principal_idRel.mp inferInstance

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