norm_ofSubsingleton — Mathlib

English

A subsingleton reduces to a standard norm equality for ContinuousAlternatingMap.

Русский

Подсокращение приводит к обычному равенству норм для ContinuousAlternatingMap.

LaTeX

$$$$\|\mathrm{norm\-ofSubsingleton}(i,f)\| = \|f\|.$$$$

Lean4

@[simp]
theorem norm_ofSubsingleton [Subsingleton ι] (i : ι) (f : E →L[𝕜] F) : ‖ofSubsingleton 𝕜 E F i f‖ = ‖f‖ :=
  ContinuousMultilinearMap.norm_ofSubsingleton i f

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