nnnorm_ofSubsingleton_id_le — Mathlib

English

If ι is a subsingleton, the NN-norm of the same evaluation map is bounded by 1.

Русский

Если ι — подмножество, состоящее из одного элемента, нормa NN-нормы того же отображения не превышает 1.

LaTeX

$$$\|\operatorname{ofSubsingleton}_{\mathbb{K}}(E,E,i,\mathrm{id}_E)\|_{\!+} \le 1$$$

Lean4

theorem nnnorm_ofSubsingleton_id_le [Subsingleton ι] (i : ι) : ‖ofSubsingleton 𝕜 E E i (.id _ _)‖₊ ≤ 1 :=
  ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le ..

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