norm_toContinuousLinearMap_le — Mathlib

English

The restriction-isometry maps, when viewed as linear maps, correspond to the standard restrictScalars construction.

Русский

Изометрии ограничения скаляров, рассматриваемые как линейные отображения, соответствуют обычному ограничению скаляров.

LaTeX

$$$ (\\mathrm{restrictScalarsIsometry}\;\\cdot)^{toLinearMap} = \\mathrm{restrictScalars} $$$

Lean4

theorem norm_toContinuousLinearMap_le (f : E →ₛₗᵢ[σ₁₂] F) : ‖f.toContinuousLinearMap‖ ≤ 1 :=
  f.toContinuousLinearMap.opNorm_le_bound zero_le_one fun x => by simp

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