norm_map_eq — Mathlib

English

If f preserves the norm, then the matrix norm after applying f equals the original matrix norm.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem norm_map_eq (A : Matrix m n α) (f : α → β) (hf : ∀ a, ‖f a‖ = ‖a‖) : ‖A.map f‖ = ‖A‖ :=
  (congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_map_eq A f fun a => Subtype.ext <| hf a :)

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