norm_def — Mathlib

English

For all E and F with norms, the norm on the product is given by the same max rule: ‖(x,y)‖ = max(‖x‖, ‖y‖).

Русский

Для произвольных нормированных E и F норма пары в произведении равна максимуму норм каждого компонента: ‖(x,y)‖ = max(‖x‖, ‖y‖).

LaTeX

$$$\|x\| = \max\|x_{\mathrm{fst}}\| \|x_{\mathrm{snd}}\|$$$

Lean4

theorem norm_def (x : E × F) : ‖x‖ = max ‖x.1‖ ‖x.2‖ :=
  rfl

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