nnnorm_toContinuousMultilinearMap

Mathlib.Analysis.NormedSpace.Alternating.Basic

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

English

The inclusion of E [⋀^ι]→L[𝕜] F into ContinuousMultilinearMap 𝕜 (ι ↦ E) F is a linear isometry.

Русский

Включение E [⋀^ι]→L[𝕜] F в ContinuousMultilinearMap 𝕜 (ι ↦ E) F является линейной изометрией.

LaTeX

$$$\text{toContinuousMultilinearMapLI}$ is a linear isometry$$

Lean4

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

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

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

Разделы

Аффилиация

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