nnnorm_def' — Mathlib

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

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