opNNNorm_prod

Mathlib.Analysis.NormedSpace.Alternating.Basic

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

English

The NNNorm of a product equals the maximum of the NNNorms of the factors.

Русский

NNNorm произведения равно максимальному NNNorm факторов.

LaTeX

$$$$\|f.prod g\|_{+} = \max(\|f\|_{+}, \|g\|_{+}).$$$$

Lean4

theorem opNNNorm_prod (f : E [⋀^ι]→L[𝕜] F) (g : E [⋀^ι]→L[𝕜] G) : ‖f.prod g‖₊ = max (‖f‖₊) (‖g‖₊) :=
  f.1.opNNNorm_prod g.1

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

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

Разделы

Аффилиация

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