instContinuousSMul — Mathlib

English

There is a canonical uniform-continuous constant scalar action by a monoid M on ContinuousMultilinearMap 𝕜 E F.

Русский

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

LaTeX

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

Lean4

instance instContinuousSMul [ContinuousSMul 𝕜 F] : ContinuousSMul 𝕜 (ContinuousMultilinearMap 𝕜 E F) :=
  letI := IsTopologicalAddGroup.toUniformSpace F
  haveI := isUniformAddGroup_of_addCommGroup (G := F)
  let φ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] (Π i, E i) → F :=
    { toFun := (↑), map_add' := fun _ _ ↦ rfl, map_smul' := fun _ _ ↦ rfl }
  UniformOnFun.continuousSMul_induced_of_image_bounded _ _ _ _ φ isEmbedding_toUniformOnFun.isInducing fun _ _ hu ↦
    hu.image_multilinear _

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