instIsUniformGroupUniformOnFun — Mathlib

English

Let 𝔖 be a set of subsets of α. If G is a uniform group, then UniformOnFun α G 𝔖 is a uniform group.

Русский

Пусть 𝔖 — семейство подмножеств α. Если G — равномерная группа, то UniformOnFun α G 𝔖 — равномерная группа.

LaTeX

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

Lean4

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

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