mapLinearIsometryEquiv — Mathlib

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

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