norm_repr_le_norm — Mathlib

English

The norm of each coefficient x_i in the basis representation is bounded by the norm of the element x.

Русский

Норма каждого коэффициента x_i в разложении по базису ограничена нормой элемента x.

LaTeX

$$$\\|B.repr\\,x\\,i\\| \\le B.norm\\,x$$$

Lean4

/-- The norm of a coefficient `x_i` is less than or equal to the norm of `x`. -/
theorem norm_repr_le_norm {x : L} (i : ι) : ‖B.repr x i‖ ≤ B.norm x :=
  Finset.le_sup' (fun i : ι ↦ ‖B.repr x i‖) (mem_univ i)

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