norm_toContinuousMultilinearMap

Mathlib.Analysis.NormedSpace.Alternating.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousAlternatingMap.norm_toContinuousMultilinearMap

English

The ENorm (extended norm) of the continuous multilinear map equals the ENorm of the alternating map.

Русский

Расширенная норма непрерывного мультилINLINE отображения равна расширенной норме чередующейся карты.

LaTeX

$$$\mathrm{enorm}(f.1) = \mathrm{enorm}(f)$$$

Lean4

@[simp]
theorem norm_toContinuousMultilinearMap (f : E [⋀^ι]→L[𝕜] F) : ‖f.1‖ = ‖f‖ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru