linfty_opNNNorm_diagonal — Mathlib

English

For a DecidableEq m, the NNNorm of diagonal v equals the NNNorm of v: ∥diagonal v∥₊ = ∥v∥₊.

Русский

При DecidableEq m нормa NNReal диагонали равна норме вектора: ∥diagonal v∥₊ = ∥v∥₊.

LaTeX

$$$\\|\\mathrm{diagonal}(v)\\|_{nn} = \\|v\\|_{nn}. $$$

Lean4

@[simp]
theorem linfty_opNNNorm_diagonal [DecidableEq m] (v : m → α) : ‖diagonal v‖₊ = ‖v‖₊ :=
  by
  rw [linfty_opNNNorm_def, Pi.nnnorm_def]
  congr 1 with i : 1
  refine (Finset.sum_eq_single_of_mem _ (Finset.mem_univ i) fun j _hj hij => ?_).trans ?_
  · rw [diagonal_apply_ne' _ hij, nnnorm_zero]
  · rw [diagonal_apply_eq]

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