continuousConstSMul — Mathlib

English

There is a natural instance of uniform continuous scalar multiplication on UniformConvergenceCLM given M with UniformContinuousConstSMul.

Русский

Существует естественный пример равномерно непрерывного умножения на скаляры на UniformConvergenceCLM, если M имеет UniformContinuousConstSMul.

LaTeX

$$$$ UniformContinuousConstSMul M (UniformConvergenceCLM_{\sigma} F \mathfrak{S}) $$$$

Lean4

instance continuousConstSMul {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F]
    [IsTopologicalAddGroup F] [ContinuousConstSMul M F] : ContinuousConstSMul M (E →SL[σ] F) :=
  UniformConvergenceCLM.instContinuousConstSMul σ F _ _

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