toContinuousMultilinearMap_curryLeft

English

Let f be a continuous alternating map in n+1 variables. The curryLeft operation commutes with converting to a continuous multilinear map, i.e., the curryLeft of f corresponds to curryLeft of f’s underlying multilinear map.

Русский

Пусть f — непрерывное чередующее отображение в n+1 переменных. Операция curryLeft после преобразования к непрерывной многообразной карте эквивалентна преобразованию curryLeft самой функции.

LaTeX

$$$ (f.curryLeft)^{toMultilinear} = f^{toMultilinear} \\text{ after curryLeft }$$$

Lean4

@[simp]
theorem toContinuousMultilinearMap_curryLeft (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (x : E) :
    (f.curryLeft x).toContinuousMultilinearMap = f.toContinuousMultilinearMap.curryLeft x :=
  rfl

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