toSubtypeRange — Mathlib

English

If v is orthonormal, then the sequence of the range of v, viewed as a family, is orthonormal.

Русский

Если v ортонормировано, то последовательность предельного диапазона v образует ортонормированную систему.

LaTeX

$$$\operatorname{Orthonormal} 𝕜 v \rightarrow \operatorname{Orthonormal} 𝕜 (\operatorname{Subtype.val} : Set.range v \to E)$$$

Lean4

/-- If `v : ι → E` is an orthonormal family, then `Subtype.val : (range v) → E` is an orthonormal
family. -/
theorem toSubtypeRange {v : ι → E} (hv : Orthonormal 𝕜 v) : Orthonormal 𝕜 (Subtype.val : Set.range v → E) :=
  (orthonormal_subtype_range hv.linearIndependent.injective).2 hv

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