nnnorm_ofSubsingleton — Mathlib

English

In the subsingleton case, the NN-norm (nonnegative-norm) of the subsingleton specialization of a map equals the NN-norm of the original map. This is the NNReal analogue of norm preservation under singleton restriction.

Русский

В случае субодинотности NN-норма (неотрицательная норма) специализации отображения на один индекс равна NN-норме исходного отображения.

LaTeX

$$$\|\mathrm{ofSubsingleton}_{\mathbb{K}}(G,G',i,f)\|_{\mathrm{nn}} = \|f\|_{\mathrm{nn}}$$

Lean4

@[simp]
theorem nnnorm_ofSubsingleton [Subsingleton ι] (i : ι) (f : G →L[𝕜] G') : ‖ofSubsingleton 𝕜 G G' i f‖₊ = ‖f‖₊ :=
  NNReal.eq <| norm_ofSubsingleton i f

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