topologicalGroup_is_uniform_of_compactSpace

English

If G is a compact topological group, then G is a uniform group.

Русский

Если G — компактная топологическая группа, то она является равномерной группой.

LaTeX

$$$[CompactSpace G] \Rightarrow IsUniformGroup\ G.$$$

Lean4

@[to_additive (attr := deprecated IsUniformGroup.of_compactSpace (since := "2025-09-27"))]
theorem topologicalGroup_is_uniform_of_compactSpace [CompactSpace G] : IsUniformGroup G :=
  inferInstance

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