norm_def — Mathlib

English

For a matrix A ∈ Matrix m n α, the matrix norm is defined as the norm of its entrywise representation, i.e., ∥A∥ = ∥(i,j) ↦ A_{ij}∥.

Русский

Для матрицы A ∈ M_{m,n}(α) норма матрицы определяется как норма функции, сопоставляющей каждой паре индексов свой элемент: ∥A∥ = ∥(i,j) ↦ A_{ij}∥.

LaTeX

$$$\|A\| = \|\big(i,j\big) \mapsto A_{ij}\|.$$$

Lean4

theorem norm_def (A : Matrix m n α) : ‖A‖ = ‖fun i j => A i j‖ :=
  rfl

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