linfty_opNorm_mulVec — Mathlib

English

For A ∈ Mat_{l×m}(α) and v ∈ α^m, the real norm of A.mulVec v is bounded by ∥A∥ ∥v∥: ∥A.mulVec v∥ ≤ ∥A∥ ∥v∥.

Русский

Для A ∈ Mat_{l×m}(α) и v ∈ α^m, вещественная норма A·v ограничена: ∥A·v∥ ≤ ∥A∥ ∥v∥.

LaTeX

$$$\\|A \\cdot v\\| \\leq \\|A\\| \\cdot \\|v\\|.$$$

Lean4

theorem linfty_opNorm_mulVec (A : Matrix l m α) (v : m → α) : ‖A *ᵥ v‖ ≤ ‖A‖ * ‖v‖ :=
  linfty_opNNNorm_mulVec _ _

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