norm_compL_le — Mathlib

English

The operator norm of the composition map compL is at most 1; in other words, composing with a fixed linear map yields a contraction of operator norm ≤ 1.

Русский

Пусть compL — отображение, которое задаёт композицию двух линейных отображений; его нормa как оператора не превышает единицу: ||compL|| ≤ 1.

LaTeX

$$$\|\operatorname{compL} \| \le 1$$$

Lean4

theorem norm_compL_le : ‖compL 𝕜 E Fₗ Gₗ‖ ≤ 1 :=
  norm_compSL_le _ _ _ _ _

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