norm_toContinuousLinearMap_comp — Mathlib

English

Precomposition with a linear isometry preserves the operator norm (dup).

Русский

Предварительное композиционное отображение с изометрией сохраняет норму оператора (повтор).

LaTeX

$$$\\|f\\circ g\\| = \\|g\\|$ for suitable isometries g.$$

Lean4

/-- Postcomposition of a continuous linear map with a linear isometry preserves
the operator norm. -/
theorem norm_toContinuousLinearMap_comp [RingHomIsometric σ₁₂] (f : F →ₛₗᵢ[σ₂₃] G) {g : E →SL[σ₁₂] F} :
    ‖f.toContinuousLinearMap.comp g‖ = ‖g‖ :=
  opNorm_ext (f.toContinuousLinearMap.comp g) g fun x => by
    simp only [norm_map, coe_toContinuousLinearMap, coe_comp', Function.comp_apply]

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