toAlternatingMap_curryLeft — Mathlib

English

The CurryLeft of a continuous alternating map corresponds to the alternating map obtained by currying, i.e., applying curryLeft to the alternating map yields the expected currying relation.

Русский

Карри-левая операция к непрерывному чередующему отображению соответствует чередующему отображению, получаемому при каррировании.

LaTeX

$$$(f.curryLeft x)^{toAlternatingMap} = f^{toAlternatingMap} \\circ x$$$

Lean4

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

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