linfty_opNorm_toMatrix — Mathlib

English

For a continuous linear map f: (RingHom.id α) → ((n → α) → α), the matrix-to-linear-map norm equals the operator norm of f.

Русский

Для непрерывного линейного отображения f: ... линейная карта по матрице имеет норму равную операторной норме f.

LaTeX

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

Lean4

@[simp]
theorem linfty_opNorm_toMatrix (f : (n → α) →L[α] (m → α)) : ‖LinearMap.toMatrix' (↑f : (n → α) →ₗ[α] (m → α))‖ = ‖f‖ :=
  congr_arg NNReal.toReal (linfty_opNNNorm_toMatrix f)

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