English
Let v be an orthonormal family of vectors, and the index set ι has size equal to the dimension finrank of E. Then the canonical basis obtained from basisOfOrthonormalOfCardEqFinrank hv card_eq coincides with v.
Русский
Пусть имеется ортонормированная совокупность векторов v индексированная ι, причём кардинал ι равен размеру базиса фин. размерности E. Тогда полученный базис basisOfOrthonormalOfCardEqFinrank hv card_eq совпадает с v.
LaTeX
$$$(basisOfOrthonormalOfCardEqFinrank\\ hv\\ card\_eq) = v$.$$
Lean4
/-- A linear map that sends an orthonormal basis to orthonormal vectors is a linear isometry. -/
def isometryOfOrthonormal (f : E →ₗ[𝕜] E') {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) (hf : Orthonormal 𝕜 (f ∘ v)) :
E →ₗᵢ[𝕜] E' :=
f.isometryOfInner fun x y => by
classical
rw [← v.linearCombination_repr x, ← v.linearCombination_repr y, Finsupp.apply_linearCombination,
Finsupp.apply_linearCombination, hv.inner_finsupp_eq_sum_left, hf.inner_finsupp_eq_sum_left]
