norm_eq_sup_sup_nnnorm — Mathlib

English

The matrix norm is the supremum of the entrywise nonnegative norms: ∥A∥ = sup_{i,j} ∥A_{ij}∥_+.

Русский

Норма матрицы равна супремуму по элементам их ненулевых норм: ∥A∥ = sup_{i,j} ∥A_{ij}∥_+.

LaTeX

$$$\|A\| = \sup_{i\in m}\sup_{j\in n} \|A_{ij}\|_+.$$$

Lean4

/-- The norm of a matrix is the sup of the sup of the nnnorm of the entries -/
theorem norm_eq_sup_sup_nnnorm (A : Matrix m n α) :
    ‖A‖ = Finset.sup Finset.univ fun i ↦ Finset.sup Finset.univ fun j ↦ ‖A i j‖₊ := by
  simp_rw [Matrix.norm_def, Pi.norm_def, Pi.nnnorm_def]

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