linfty_opNorm_eq_opNorm — Mathlib

English

For a linear map f: (n → α) → (m → α), the operator norm of the associated matrix-to-linear-map conversion equals the operator norm of f itself.

Русский

Для линейного отображения f: (n → α) → (m → α) нормa конвертации в матрицу эквивалентной линейной карте равна норме самой карты f.

LaTeX

$$$\|\mathrm{toMatrix}'(\uparrow f)\| = \|f\|.$$$

Lean4

theorem linfty_opNorm_eq_opNorm (A : Matrix m n α) : ‖A‖ = ‖ContinuousLinearMap.mk (Matrix.mulVecLin A)‖ :=
  congr_arg NNReal.toReal (linfty_opNNNorm_eq_opNNNorm A)

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