opNorm_prod

Mathlib.Analysis.NormedSpace.Alternating.Basic

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

English

The operator norm of the product equals the maximum of the operator norms of the factors.

Русский

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

LaTeX

$$$$\|f.prod g\| = \max(\|f\|, \|g\|).$$$$

Lean4

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

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

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

Разделы

Аффилиация

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