curryLeft_compContinuousAlternatingMap

English

CurryLeft as a linear isometry is defined by providing the required norm preservation data.

Русский

CurryLeft задается как линейная изометрия через сохранение нормы.

LaTeX

$$defined as above$$

Lean4

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

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