le_opNorm₂ — Mathlib

English

The coerced restriction-isometry equals the restriction map when viewed as a linear map.

Русский

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

LaTeX

$$$ \mathrm{coe\_restrictScalarsIsometry} = \mathrm{restrictScalars} $$$

Lean4

theorem le_opNorm₂ [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F) : ‖f x y‖ ≤ ‖f‖ * ‖x‖ * ‖y‖ :=
  (f x).le_of_opNorm_le (f.le_opNorm x) y

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