norm_mk — Mathlib

English

In a product of normed spaces E×F with the product norm, the norm of a pair (x,y) is the maximum of the two component norms: ∥(x,y)∥ = max(∥x∥, ∥y∥).

Русский

В произведении нормированных пространств E×F с нормой-образом пара (x,y) имеет норму ∥(x,y)∥ = max(∥x∥, ∥y∥).

LaTeX

$$$\|(x,y)\| = \max(\|x\|,\|y\|).$$$

Lean4

@[simp]
theorem norm_mk (x : E) (y : F) : ‖(x, y)‖ = max ‖x‖ ‖y‖ :=
  rfl

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