linftyOpNonUnitalSemiNormedRing — Mathlib

English

Same as above but in NNReal terms: ∥A.mulVec v∥₊ ≤ ∥A∥₊ ∥v∥₊.

Русский

То же самое в терминах NNReal: ∥A·v∥₊ ≤ ∥A∥₊ ∥v∥₊.

LaTeX

$$$\\|A \\cdot v\\|_{nn} \\leq \\|A\\|_{nn} \\cdot \\|v\\|_{nn}.$$$

Lean4

/-- Seminormed non-unital ring instance (using sup norm of L1 norm) for matrices over a semi normed
non-unital ring. Not declared as an instance because there are several natural choices for defining
the norm of a matrix. -/
@[local instance]
protected def linftyOpNonUnitalSemiNormedRing [NonUnitalSeminormedRing α] : NonUnitalSeminormedRing (Matrix n n α) :=
  { Matrix.linftyOpSeminormedAddCommGroup, Matrix.instNonUnitalRing with norm_mul_le := linfty_opNorm_mul }

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