linfty_opNorm_replicateCol — Mathlib

English

Similarly, the real norm of replicateCol ι v equals the real norm of v: ∥replicateCol ι v∥ = ∥v∥.

Русский

Аналогично, вещественная норма replicateCol ι v равна норме v: ∥replicateCol ι v∥ = ∥v∥.

LaTeX

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

Lean4

@[simp]
theorem linfty_opNorm_replicateCol (v : m → α) : ‖replicateCol ι v‖ = ‖v‖ :=
  congr_arg ((↑) : ℝ≥0 → ℝ) <| linfty_opNNNorm_replicateCol v

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