instIsUniformGroup — Mathlib

English

If G is a group with a uniform structure and the group operations are uniformly continuous, then the separation quotient of G is itself a uniform group.

Русский

Если G — группа с равномерной структурой и операции группы uniformly continuous, то разделительная фактор-группа G сама образует равномерную группу.

LaTeX

$$$IsUniformGroup\left(\mathrm{SeparationQuotient}(G)\right)$$$

Lean4

@[to_additive]
instance instIsUniformGroup {G : Type*} [Group G] [UniformSpace G] [IsUniformGroup G] :
    IsUniformGroup (SeparationQuotient G) where
  uniformContinuous_div := by
    rw [uniformContinuous_dom₂]
    exact uniformContinuous_mk.comp uniformContinuous_div

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