toUniformSpace_eq — Mathlib

English

The canonical uniform space associated to an IsUniformGroup coincides with the given one.

Русский

Каноническая униформное пространство, связанное с IsUniformGroup, совпадает с данным.

LaTeX

$$$IsTopologicalGroup.toUniformSpace G = u$$$

Lean4

@[to_additive]
theorem toUniformSpace_eq {G : Type*} [u : UniformSpace G] [Group G] [IsUniformGroup G] :
    IsTopologicalGroup.toUniformSpace G = u := by
  ext : 1
  rw [uniformity_eq_comap_nhds_one' G, uniformity_eq_comap_nhds_one G]

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