norm_compContinuousAlternatingMap_le

English

Restriction of scalars preserves the norm of a continuous alternating map after a left restriction

Русский

Ограничение скаляров слева сохраняет норму непрерывного чередующего отображения после левого ограничения

LaTeX

$$$\|f.restrictScalars 𝕜'\| = \|f\|$$$

Lean4

theorem norm_compContinuousAlternatingMap_le (g : F →L[𝕜] G) (f : E [⋀^ι]→L[𝕜] F) :
    ‖g.compContinuousAlternatingMap f‖ ≤ ‖g‖ * ‖f‖ :=
  g.norm_compContinuousMultilinearMap_le f.1

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