compContinuousAlternatingMapCLM — Mathlib

English

Composing a continuous linear map with a continuous alternating map yields a continuous linear map whose operator norm is controlled by the operator norm of the linear map and the norm of the alternating map.

Русский

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

LaTeX

$$$\|g.\mathrm{compContinuousAlternatingMap}(f)\| \le \|g\| \cdot \|f\|$$$

Lean4

/-- `ContinuousLinearMap.compContinuousAlternatingMap` as a bundled continuous bilinear map. -/
@[simps! apply_apply]
def compContinuousAlternatingMapCLM : (F →L[𝕜] G) →L[𝕜] (E [⋀^ι]→L[𝕜] F) →L[𝕜] (E [⋀^ι]→L[𝕜] G) :=
  LinearMap.mkContinuous₂ (compContinuousAlternatingMapₗ 𝕜 E F G) 1 fun f g ↦ by
    simpa using f.norm_compContinuousAlternatingMap_le g

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