norm_compContinuousAlternatingMap

English

Composition with an isomorphism preserves norm of maps up to norm of the isomorphism.

Русский

Сочетание c изоморфизмом сохраняет норму отображений в пределах нормы изоморфизма.

LaTeX

$$$\|g\cdot f\| = \|g\| \cdot \|f\|$ in appropriate contexts$$

Lean4

theorem norm_compContinuousAlternatingMap (g : F →ₗᵢ[𝕜] G) (f : E [⋀^ι]→L[𝕜] F) :
    ‖g.toContinuousLinearMap.compContinuousAlternatingMap f‖ = ‖f‖ :=
  g.norm_compContinuousMultilinearMap f.1

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