uniformContinuous_toContinuousMultilinearMap

English

The map toContinuousMultilinearMap is uniformly continuous as it is the composition of two uniform-structure-preserving maps: the isUniformEmbedding and the canonical evaluation.

Русский

Отображение toContinuousMultilinearMap равномерно непрерывно, поскольку оно является композицией отображений, сохраняющих униформную структуру: из UniformEmbedding и канонической оценки.

LaTeX

$$$$ UniformContinuous (toContinuousMultilinearMap) $$$$

Lean4

theorem uniformContinuous_toContinuousMultilinearMap :
    UniformContinuous (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F) → _) :=
  isUniformEmbedding_toContinuousMultilinearMap.uniformContinuous

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