instIsUniformGroupUniformFun — Mathlib

English

If G is a uniform group, then the function space UniformFun α G is also a uniform group.

Русский

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

LaTeX

$$$\text{IsUniformGroup } G \rightarrow \text{IsUniformGroup } (\mathrm{UniformFun} \; α \; G).$$$

Lean4

/-- If `G` is a uniform group, then `α →ᵤ G` is a uniform group as well. -/
@[to_additive /-- If `G` is a uniform additive group,
    then `α →ᵤ G` is a uniform additive group as well. -/
    ]
instance : IsUniformGroup (α →ᵤ G) :=
  ⟨(UniformFun.postcomp_uniformContinuous uniformContinuous_div).comp
      UniformFun.uniformEquivProdArrow.symm.uniformContinuous⟩

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