instUniformContinuousConstSMul — Mathlib

English

There is a uniform continuous constant-scalar action of any monoid M on ContinuousMultilinearMap 𝕜 E F, provided suitable structures on F and E_i.

Русский

Существует равномерно непрерывное глобальное умножение константного скаляра со стороны моноида M на ContinuousMultilinearMap 𝕜 E F при наличии соответствующих структур.

LaTeX

$$UniformContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)$$

Lean4

instance instUniformContinuousConstSMul {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F]
    [ContinuousConstSMul M F] : UniformContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F) :=
  haveI := uniformContinuousConstSMul_of_continuousConstSMul M F
  isUniformEmbedding_toUniformOnFun.uniformContinuousConstSMul fun _ _ ↦ rfl

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