linfty_opNorm_diagonal — Mathlib

English

For a DecidableEq m, the real norm of diagonal v equals the real norm of v: ∥diagonal v∥ = ∥v∥.

Русский

При DecidableEq m вещественная норма диагонали равна норме вектора: ∥diagonal v∥ = ∥v∥.

LaTeX

$$$\\|\\mathrm{diagonal}(v)\\| = \\|v\\|$$$

Lean4

@[simp]
theorem linfty_opNorm_diagonal [DecidableEq m] (v : m → α) : ‖diagonal v‖ = ‖v‖ :=
  congr_arg ((↑) : ℝ≥0 → ℝ) <| linfty_opNNNorm_diagonal v

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