linfty_opNNNorm_replicateCol — Mathlib

English

For a vector v, the NNNorm of replicateCol ι v is equal to the NNNorm of v: ∥replicateCol ι v∥₊ = ∥v∥₊.

Русский

Для вектора v нормa NNReal матрицы replicateCol ι v равна норме v: ∥replicateCol ι v∥₊ = ∥v∥₊.

LaTeX

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

Lean4

@[simp]
theorem linfty_opNNNorm_replicateCol (v : m → α) : ‖replicateCol ι v‖₊ = ‖v‖₊ :=
  by
  rw [linfty_opNNNorm_def, Pi.nnnorm_def]
  simp

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