English
A linear equivalence that sends an orthonormal basis to an orthonormal basis is itself a linear isometry.
Русский
Линейное эквивалентное отображение, переводящее ортонормированный базис в ортонормированный базис, является линейной изометрией.
LaTeX
$$$\\text{If } v \\text{ is orthonormal and } f: E \\simeq E'\\text{ with } f \\circ v \\text{ orthonormal, then } f\\text{ is a linear isometry}.$$$
Lean4
/-- A linear equivalence that sends an orthonormal basis to orthonormal vectors is a linear
isometric equivalence. -/
def isometryOfOrthonormal (f : E ≃ₗ[𝕜] E') {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) (hf : Orthonormal 𝕜 (f ∘ v)) :
E ≃ₗᵢ[𝕜] E' :=
f.isometryOfInner fun x y => by
rw [← LinearEquiv.coe_coe] at hf
classical
rw [← v.linearCombination_repr x, ← v.linearCombination_repr y, ← LinearEquiv.coe_coe f,
Finsupp.apply_linearCombination, Finsupp.apply_linearCombination, hv.inner_finsupp_eq_sum_left,
hf.inner_finsupp_eq_sum_left]
