instIsUniformGroup — Mathlib

English

If each G(i) is a uniform group, then the function space ∀i G(i) is a uniform group with the usual product uniformity.

Русский

Если для каждого i группа G(i) является равномерной, то пространство функций ∀i G(i) образует равномерную группу.

LaTeX

$$$\big(\forall i, IsUniformGroup (G(i))\big) \Rightarrow IsUniformGroup (\forall i, G(i)).$$$

Lean4

@[to_additive]
instance instIsUniformGroup {ι : Type*} {G : ι → Type*} [∀ i, UniformSpace (G i)] [∀ i, Group (G i)]
    [∀ i, IsUniformGroup (G i)] : IsUniformGroup (∀ i, G i) :=
  by
  rw [Pi.uniformSpace_eq]
  exact isUniformGroup_iInf fun i ↦ .comap (Pi.evalMonoidHom G i)

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