English
If v is an orthonormal basis (in the sense of an orthonormal basis), then applying a linear isometry equivalence preserves orthonormality of the mapped basis.
Русский
Если имеется ортонормированный базис, то применение линейной изометрической эквивалентности сохраняет ортонормированность отображённого базиса.
LaTeX
$$$\\operatorname{Orthonormal}_{\\mathbb{K}}(v) \\Rightarrow \\operatorname{Orthonormal}_{\\mathbb{K}}(v.map f.toLinearEquiv)$ for a linear isometry equivalence $f$.$$
Lean4
/-- A linear isometric equivalence, applied with `Basis.map`, preserves the property of being
orthonormal. -/
theorem mapLinearIsometryEquiv {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) (f : E ≃ₗᵢ[𝕜] E') :
Orthonormal 𝕜 (v.map f.toLinearEquiv) :=
hv.comp_linearIsometryEquiv f