uniformContinuous_coe_fun — Mathlib

English

The evaluation map that sends a multilinear map to its values is uniformly continuous with respect to the appropriate topologies.

Русский

Функция, оценивающая значения мультилíneарного отображения, является равномерно непрерывной в соответствующих топологиях.

LaTeX

$$UniformContinuous (DFunLike.coe : ContinuousMultilinearMap 𝕜 E F → (Π i, E i) → F)$$

Lean4

theorem uniformContinuous_coe_fun [∀ i, ContinuousSMul 𝕜 (E i)] :
    UniformContinuous (DFunLike.coe : ContinuousMultilinearMap 𝕜 E F → (Π i, E i) → F) :=
  (UniformOnFun.uniformContinuous_toFun isVonNBounded_covers).comp isUniformEmbedding_toUniformOnFun.uniformContinuous

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