linfty_opNNNorm_replicateRow — Mathlib

English

For v : n → α, the NNNorm of replicateRow ι v equals the sum of NNNorms of components: ∥replicateRow ι v∥₊ = ∑_i ∥v_i∥₊.

Русский

Для v : n → α нормa NNReal матрицы replicateRow ι v равна сумме норм элементов: ∥replicateRow ι v∥₊ = ∑_i ∥v_i∥₊.

LaTeX

$$$\\|\\mathrm{replicateRow}_{\\iota} (v)\\|_{nn} = \\sum_{i\\in n} \\|v_i\\|_{nn}.$$$

Lean4

@[simp]
theorem linfty_opNNNorm_replicateRow (v : n → α) : ‖replicateRow ι v‖₊ = ∑ i, ‖v i‖₊ := by simp [linfty_opNNNorm_def]

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