curryLeft_compContinuousLinearMap

English

For a continuous alternating map f, inserting x at position p in v yields, up to sign (-1)^{p}, the evaluated value on the augmented vector.

Русский

При вставке элемента x на позицию p в вектор v выражение оценивается как (-1)^p умноженное на f на расширенном векторе.

LaTeX

$$$(-1)^{p} \\cdot f(p.insertNth x v) = f(Matrix.vecCons x v)$$$

Lean4

@[simp]
theorem curryLeft_compContinuousLinearMap (g : F [⋀^Fin (n + 1)]→L[𝕜] G) (f : E →L[𝕜] F) (x : E) :
    (g.compContinuousLinearMap f).curryLeft x = (g.curryLeft (f x)).compContinuousLinearMap f :=
  ext fun v ↦ congr_arg g <| funext fun i ↦ by cases i using Fin.cases <;> simp

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