English
Let ι be a finite index set and consider the Euclidean space with coordinates indexed by ι. For any index i and any scalar a in 𝕜, the vector that has a in the i-th coordinate and zeros elsewhere has NN-norm equal to the NN-norm of a; i.e. the i-th coordinate embedding preserves nn-norm.
Русский
Пусть ι — конечное множество индексов. В евклидовом пространстве с координатами по индексам ι для любой i∈ι и любого скаляра a∈𝕜 вектор, у которого в i-й координате стоит a, а во всех остальных координатах ноль, имеет NN-норму, равную NN-норме a.
LaTeX
$$$\|\mathrm{EuclideanSpace}.single(i, a)\|_{+} = \|a\|_{+}$$$
Lean4
@[simp]
theorem nnnorm_single (i : ι) (a : 𝕜) : ‖EuclideanSpace.single i (a : 𝕜)‖₊ = ‖a‖₊ :=
PiLp.nnnorm_toLp_single 2 (fun _ => 𝕜) i a
