instContinuousConstSMul — Mathlib

English

If a space F carries a continuous action by a monoid M, then the space of continuous alternating maps inherits a continuous scalar action by M.

Русский

Если пространство F имеет непрерывное действие моноида M, то пространство непрерывных чередующихся отображений наследует непрерывное действие M.

LaTeX

$$$\\forall M:\\text{Monoid},\\; [ContinuousConstSMul\\; M\\; F]\\Rightarrow [ContinuousConstSMul\\; M\\; (E [⋀^ι]→L_{𝕜} F)]$$$

Lean4

instance instContinuousConstSMul {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F]
    [ContinuousConstSMul M F] : ContinuousConstSMul M (E [⋀^ι]→L[𝕜] F) :=
  isEmbedding_toContinuousMultilinearMap.continuousConstSMul id rfl

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