uniformContinuous_coe_fun — Mathlib

English

The evaluation functional that maps a continuous alternating map to its values at a finite family of inputs is uniformly continuous.

Русский

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

LaTeX

$$$$ UniformContinuous (DFunLike.coe : (E [⋀^ι]→L[𝕜] F) → (ι → E) → F). $$$$

Lean4

theorem uniformContinuous_coe_fun [ContinuousSMul 𝕜 E] :
    UniformContinuous (DFunLike.coe : (E [⋀^ι]→L[𝕜] F) → (ι → E) → F) :=
  ContinuousMultilinearMap.uniformContinuous_coe_fun.comp uniformContinuous_toContinuousMultilinearMap

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