norm_nonneg — Mathlib

English

Let B be a K-basis of L. For every x in L, B.norm x is nonnegative.

Русский

Пусть B — K-базис пространства L над K. Для каждого x ∈ L выполняется B.norm x ≥ 0.

LaTeX

$$$\forall x \in L,\ 0 \le B.norm(x)$$$

Lean4

/-- For any `K`-basis of `L`, and any `x : L`, we have `0 ≤ B.norm x`. -/
protected theorem norm_nonneg (x : L) : 0 ≤ B.norm x := by
  simp only [norm, le_sup'_iff, mem_univ, norm_nonneg, and_self, exists_const]

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