nnnorm_mk' — Mathlib

English

Multiplicative version of the mk-norm for pair: ‖(x,y)‖₊ = max ‖x‖₊ ‖y‖₊.

Русский

Мультипликативная версия нормы пары: ‖(x,y)‖₊ = max ‖x‖₊ ‖y‖₊.

LaTeX

$$$‖(x,y)‖_{+} = \max\,‖x‖_{+} \‖y‖_{+}$$$

Lean4

/-- Multiplicative version of `Prod.nnnorm_mk`. -/
@[to_additive (attr := simp) Prod.nnnorm_mk]
theorem nnnorm_mk' (x : E) (y : F) : ‖(x, y)‖₊ = max ‖x‖₊ ‖y‖₊ :=
  rfl

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