nnnorm_eq_one — Mathlib

English

If v is orthonormal, then the nonnegative norm (NNNorm) of each vector v_i equals 1: ‖v_i‖₊ = 1.

Русский

Если v ортонормированно, то для каждого i ∥v_i∥₊ = 1.

LaTeX

$$$\operatorname{Orthonormal} 𝕜 v \rightarrow \forall i, \|v i\|_{nn} = 1$$$

Lean4

theorem nnnorm_eq_one {v : ι → E} (h : Orthonormal 𝕜 v) (i : ι) : ‖v i‖₊ = 1 :=
  by
  suffices (‖v i‖₊ : ℝ) = 1 by norm_cast at this
  simp [h.norm_eq_one]

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