curryLeftLI — Mathlib

English

The curryLeft operation, viewed as a map from continuous alternating maps to continuous linear maps, is a linear isometry.

Русский

Операция curryLeft рассматривается как линейное изометрическое отображение.

LaTeX

$$$curryLeftLI : (E [⋀^Fin (n+1)]→L[𝕜] F) \\toₗᵢ[𝕜] (E →L[𝕜] E [⋀^Fin n]→L[𝕜] F)$ is an isometry.$$

Lean4

/-- `ContinuousAlternatingMap.curryLeft` as a `LinearIsometry`. -/
@[simps]
noncomputable def curryLeftLI : (E [⋀^Fin (n + 1)]→L[𝕜] F) →ₗᵢ[𝕜] (E →L[𝕜] E [⋀^Fin n]→L[𝕜] F)
    where
  toFun f := f.curryLeft
  map_add' := curryLeft_add
  map_smul' := curryLeft_smul
  norm_map' := norm_curryLeft

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