norm_ofSubsingleton — Mathlib

English

If the index set ι is a subsingleton, then the norm of the map obtained by restricting to that singleton index coincides with the norm of the original linear map. This reflects that with only one coordinate, the multilinear structure collapses to a linear map without loss of norm.

Русский

Если множество индексов ι имеет единственный элемент, то норма отображения, полученного из единственного индекса, совпадает с нормой исходного линейного отображения.

LaTeX

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

Lean4

@[simp]
theorem norm_ofSubsingleton [Subsingleton ι] (i : ι) (f : G →L[𝕜] G') : ‖ofSubsingleton 𝕜 G G' i f‖ = ‖f‖ :=
  by
  letI : Unique ι := uniqueOfSubsingleton i
  simp [norm_def, ContinuousLinearMap.norm_def, (Equiv.funUnique _ _).symm.surjective.forall]

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