instL2OpNormedAddCommGroup — Mathlib

English

Equivalent definition of the nn-norm using the induced linear identification with Euclidean CLM.

Русский

Эквивалентное определение nn-нормы через индукцию линейного отображения.

LaTeX

$$$\\|A\\|_+ = \\|(toEuclideanLin.trans toContinuousLinearMap)A\\|_+$$$

Lean4

/-- The norm structure on `Matrix m n 𝕜` arising from the operator norm given by the identification
with (continuous) linear maps of `EuclideanSpace`. -/
def instL2OpNormedAddCommGroup : NormedAddCommGroup (Matrix m n 𝕜)
    where
  norm := l2OpNormedAddCommGroupAux.norm
  dist_eq := l2OpNormedAddCommGroupAux.dist_eq

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