enorm_toContinuousMultilinearMap — Mathlib

English

The norm of the continuous alternating map and its continuous multilinear map representation agree.

Русский

Норма непрерывной чередующейся карты совпадает с нормой её представления как непрерывной мультилейной карты.

LaTeX

$$$\|f\| = \|\mathrm{toContinuousMultilinearMap}(f)\|$$$

Lean4

@[simp]
theorem enorm_toContinuousMultilinearMap (f : E [⋀^ι]→L[𝕜] F) : ‖f.1‖ₑ = ‖f‖ₑ :=
  rfl

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