linfty_opNorm_replicateRow — Mathlib

English

Similarly, the real norm of replicateRow ι v equals the sum of real norms: ∥replicateRow ι v∥ = ∑_i ∥v_i∥.

Русский

Аналогично, вещественная норма replicateRow ι v равна сумме норм элементов: ∥replicateRow ι v∥ = ∑_i ∥v_i∥.

LaTeX

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

Lean4

@[simp]
theorem linfty_opNorm_replicateRow (v : n → α) : ‖replicateRow ι v‖ = ∑ i, ‖v i‖ :=
  (congr_arg ((↑) : ℝ≥0 → ℝ) <| linfty_opNNNorm_replicateRow v).trans <| by simp [NNReal.coe_sum]

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