English
Multiplicative version of the product norm: for x ∈ E × F, the nnreal norm equals the maximum of the nnreal norms of the components.
Русский
Умноженная версия нормы произведения: для x ∈ E × F nnreal-норма равна максимуму nnreal-норм компонентов.
LaTeX
$$$‖x‖_{+} = \max\,‖x_{1}‖_{+} \,‖x_{2}‖_{+}$$$
Lean4
/-- Multiplicative version of `Prod.nnnorm_def`.
Earlier, this names was used for the additive version. -/
@[to_additive Prod.nnnorm_def]
theorem nnnorm_def' (x : E × F) : ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊ :=
rfl