compContinuousLinearMapCLM — Mathlib

English

The norm of an applied continuous alternating map respects the product of the involved norms.

Русский

Норма применённого непрерывного чередующего отображения соответствует произведению норм вовлечённых отображений.

LaTeX

$$$\|f g\| \le \|f\| \cdot \|g\|$$$

Lean4

/-- Composition of a continuous alternating map and a continuous linear map
as a bundled continuous linear map. -/
def compContinuousLinearMapCLM (f : E →L[𝕜] F) : (F [⋀^ι]→L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] G) :=
  LinearMap.mkContinuous (ContinuousAlternatingMap.compContinuousLinearMapₗ f) (‖f‖ ^ Fintype.card ι) fun g ↦
    (g.norm_compContinuousLinearMap_le f).trans_eq (mul_comm _ _)

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