norm_def' — Mathlib

English

In a finite product of seminormed groups, the norm of a function f: ι → G_i is the real number given by the supremum over i of the NNNorm of f(i), i.e., the maximum norm among the components.

Русский

В конечном произведении полумонормированных групп норма функции f: ι → G_i равна числу наибольшей нормы её компонент.

LaTeX

$$$\|f\| = \max_{i} \|f(i)\|$ (в вещественном представлении через NNNorm)$$

Lean4

@[to_additive Pi.norm_def]
theorem norm_def' : ‖f‖ = ↑(Finset.univ.sup fun b => ‖f b‖₊) :=
  rfl

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