linfty_opNNNorm_toMatrix — Mathlib

English

Let f be a bounded linear map. Then the nonnegative NN-norm of its matrix representation equals the NN-norm of f.

Русский

Пусть f — ограниченное линейное отображение. Тогда nnnorm матричного представления f совпадает с nnnorm самой карты f.

LaTeX

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

Lean4

@[simp]
theorem linfty_opNNNorm_toMatrix (f : (n → α) →L[α] (m → α)) :
    ‖LinearMap.toMatrix' (↑f : (n → α) →ₗ[α] (m → α))‖₊ = ‖f‖₊ :=
  by
  rw [linfty_opNNNorm_eq_opNNNorm]
  simp only [← toLin'_apply', toLin'_toMatrix']

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