to_uniformContinuousConstSMul — Mathlib

English

Any uniform inducing group G yields a uniform continuous constant-smul structure on G with itself as module.

Русский

Любая равномерно индуцированная группа G образует равномерно непрерывное константное действие на саму себя как модуль.

LaTeX

$$$IsUniformGroup G \Rightarrow UniformContinuousConstSMul G G$$$

Lean4

@[to_additive]
instance to_uniformContinuousConstSMul {G : Type u} [Group G] [UniformSpace G] [IsUniformGroup G] :
    UniformContinuousConstSMul G G :=
  ⟨fun _ => uniformContinuous_const.mul uniformContinuous_id⟩

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