English
A family indexed by a set equals an orthonormal family of the subtype range if and only if the original indexed family is orthonormal and injectively indexed.
Русский
Семейство, индексированное по набору, ортонормированно на диапазоне подтипов тогда и только тогда, когда исходное индексированное семейство ортонормировано и инъективно по индексу.
LaTeX
$$$\operatorname{Orthonormal} 𝕜 (\operatorname{Subtype.val} : Set.range v \to E) \iff \operatorname{Orthonormal} 𝕜 v$$$
Lean4
/-- The inner product of a linear combination of a set of orthonormal vectors with one of those
vectors picks out the coefficient of that vector. -/
theorem inner_left_finsupp {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) :
⟪linearCombination 𝕜 v l, v i⟫ = conj (l i) := by rw [← inner_conj_symm, hv.inner_right_finsupp]
