norm — Mathlib

English

For any K-basis B of L, the norm of the zero vector is zero: B.norm 0 = 0.

Русский

Для любой K-базы B пространства L норма нулевого вектора равна нулю: B.norm 0 = 0.

LaTeX

$$$B.norm\\,0 = 0$$$

Lean4

/-- The function sending an element `x : L` to the maximum of the norms of its coefficients
with respect to the `K`-basis `B` of `L`. -/
def norm (x : L) : ℝ :=
  Finset.sup' univ univ_nonempty (fun i : ι ↦ ‖B.repr x i‖)

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