instContinuousEvalConst — Mathlib

English

There is a canonical continuous evaluation-at-a fixed argument map from the space of continuous alternating maps to the underlying function space, giving a continuous linear functional for each fixed argument.

Русский

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

LaTeX

$$$\\text{ContinuousEvalConst}$$$

Lean4

instance instContinuousEvalConst : ContinuousEvalConst (E [⋀^ι]→L[𝕜] F) (ι → E) F :=
  .of_continuous_forget continuous_toContinuousMultilinearMap

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