isUniformGroup_of_commGroup — Mathlib

English

A commutative group carries an IsUniformGroup structure compatible with its topology.

Русский

Коммутативная группа несет совместную структуру IsUniformGroup, совместимую с топологией.

LaTeX

$$IsUniformGroup G$$

Lean4

@[to_additive]
theorem isUniformGroup_of_commGroup : IsUniformGroup G :=
  by
  constructor
  simp only [UniformContinuous, uniformity_prod_eq_prod, uniformity_eq_comap_nhds_one', tendsto_comap_iff,
    tendsto_map'_iff, prod_comap_comap_eq, Function.comp_def, div_div_div_comm _ (Prod.snd (Prod.snd _)),
    ← nhds_prod_eq]
  exact (continuous_div'.tendsto' 1 1 (div_one 1)).comp tendsto_comap

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