instUniformContinuousConstSMul — Mathlib

English

Under a coherence assumption with von Neumann bounded sets, the space of continuous alternating maps into a complete space F is complete.

Русский

При условии когерентности относительно ограниченных множеств двойственного типа, пространство непрерывных чередующих отображений в полное пространство F полно.

LaTeX

$$$$ \\text{completeSpace} \\; (\\text{ContinuousAlternatingMap } 𝕜 E F ι) $$$$

Lean4

instance instUniformContinuousConstSMul {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F]
    [ContinuousConstSMul M F] : UniformContinuousConstSMul M (E [⋀^ι]→L[𝕜] F) :=
  isUniformEmbedding_toContinuousMultilinearMap.uniformContinuousConstSMul fun _ _ ↦ rfl

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