instIsUniformGroup — Mathlib

English

If G and H are uniform groups, then their product G × H is a uniform group.

Русский

Если G и H — равномерные группы, то их произведение G × H также является равномерной группой.

LaTeX

$$$\text{IsUniformGroup } G \times H$.$$

Lean4

@[to_additive]
instance instIsUniformGroup [UniformSpace G] [hG : IsUniformGroup G] [UniformSpace H] [hH : IsUniformGroup H] :
    IsUniformGroup (G × H) := by
  rw [instUniformSpaceProd]
  exact isUniformGroup_inf (.comap <| MonoidHom.fst G H) (.comap <| MonoidHom.snd G H)

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