norm_curryLeft — Mathlib

English

The operator norm of the curryLeft of a continuous alternating map equals the operator norm of the map itself.

Русский

Норма оператора curryLeft непрерывного чередующего отображения равна норме самого отображения.

LaTeX

$$$\\|f.curryLeft\\| = \\|f\\|$$$

Lean4

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

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