instL2OpNormedSpace — Mathlib

English

The NN-norm is submultiplicative: ∥AB∥NN ≤ ∥A∥NN ∥B∥NN.

Русский

NN-норма субумножаема: ∥AB∥NN ≤ ∥A∥NN ∥B∥NN.

LaTeX

$$$\\forall A: M_{m\\times n}(\\mathbb{C}), B: M_{n\\times \\ell}(\\mathbb{C}), \\\\ \\|A B\\|_{NN} \\leq \\|A\\|_{NN} \\cdot \\|B\\|_{NN}$$$

Lean4

/-- The normed algebra structure on `Matrix n n 𝕜` arising from the operator norm given by the
identification with (continuous) linear endmorphisms of `EuclideanSpace 𝕜 n`. -/
def instL2OpNormedSpace : NormedSpace 𝕜 (Matrix m n 𝕜) where
  norm_smul_le r
    x := by
    rw [l2_opNorm_def, LinearEquiv.map_smul]
    exact norm_smul_le r ((toEuclideanLin (𝕜 := 𝕜) (m := m) (n := n)).trans toContinuousLinearMap x)

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