English
Let R be a normed field and α a normed space. Then Matrix m×n α carries a NormedSpace structure over R with the Linfty-operator norm, i.e., the natural sup-norm derived from the row-wise L1-norm.
Русский
Пусть R — нормированное поле, α — нормированное пространство. Тогда M_{m×n}(α) является NormedSpace над R и оснащено нормой Linfty-оператора, полученной как суп по строкам по L1-норме.
LaTeX
$$$\\text{NormedSpace } R (\\mathrm{Mat}_{m\\times n}(\\alpha))$$$
Lean4
/-- Normed space instance (using sup norm of L1 norm) for matrices over a normed space. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
@[local instance]
protected def linftyOpNormedSpace [NormedField R] [SeminormedAddCommGroup α] [NormedSpace R α] :
NormedSpace R (Matrix m n α) :=
(by infer_instance : NormedSpace R (m → PiLp 1 fun j : n => α))
