nnnorm_map_eq — Mathlib

English

If f preserves norms, then the nn-norm of A.map f equals the nn-norm of A.

Русский

Если отображение f сохраняет норму, то nnnorm матрицы A, применённой к f, равна nnnorm самой A.

LaTeX

$$$\|A.map f\|_+ = \|A\|_+\quad\text{при }\forall a, \|f(a)\|_+ = \|a\|_+.$$$

Lean4

@[simp]
theorem nnnorm_map_eq (A : Matrix m n α) (f : α → β) (hf : ∀ a, ‖f a‖₊ = ‖a‖₊) : ‖A.map f‖₊ = ‖A‖₊ := by
  simp only [nnnorm_def, Pi.nnnorm_def, Matrix.map_apply, hf]

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