English
The evaluation map on the space of continuous alternating maps is continuous in the pair (map, vector).
Русский
Классическая оценочная карта на пространстве непрерывных чередующихся отображений непрерывна в паре (отображение, вектор).
LaTeX
$$$\mathrm{ContinuousEval} \big( E [⋀^ι]→_ {\;𝕜} F\big) (ι \to E) F$$$
Lean4
/-- Applying a continuous alternating map to a vector is continuous
in the pair (map, vector).
Continuity in the vector holds by definition
and continuity in the map holds if both the domain and the codomain are topological vector spaces.
However, continuity in the pair (map, vector) needs the domain to be a locally bounded TVS.
We have no typeclass for a locally bounded TVS,
so we require it to be a seminormed space instead. -/
instance instContinuousEval {𝕜 ι E F : Type*} [NormedField 𝕜] [Finite ι] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
[TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module 𝕜 F] :
ContinuousEval (E [⋀^ι]→L[𝕜] F) (ι → E) F :=
.of_continuous_forget continuous_toContinuousMultilinearMap
