map_linearIsometryEquiv' — Mathlib

English

Variant of the above: under a linear isometry equivalence f, the HasOrthogonalProjection property is preserved for the mapped subspace.

Русский

Вариант предыдущего: под линейной изометрией-эквидивариантом f сохраняется свойство HasOrthogonalProjection для образа подпространства.

LaTeX

$$map_linearIsometryEquiv' preserves HasOrthogonalProjection$$

Lean4

instance map_linearIsometryEquiv' [K.HasOrthogonalProjection] {E' : Type*} [NormedAddCommGroup E']
    [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') : (K.map f.toLinearIsometry).HasOrthogonalProjection :=
  HasOrthogonalProjection.map_linearIsometryEquiv K f

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