map_linearIsometryEquiv — Mathlib

English

If K has an orthogonal projection and f is a linear isometry between E and E', then the image of K under f also has an orthogonal projection.

Русский

Если K имеет ортогональную проекцию и f — линейный изоморфизм-изометрия, то образ K под f имеет ортогональную проекцию.

LaTeX

$$map f : K.HasOrthogonalProjection → (K.map f) .HasOrthogonalProjection$$

Lean4

instance map_linearIsometryEquiv [K.HasOrthogonalProjection] {E' : Type*} [NormedAddCommGroup E']
    [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') : (K.map (f.toLinearEquiv : E →ₗ[𝕜] E')).HasOrthogonalProjection where
  exists_orthogonal
    v := by
    rcases HasOrthogonalProjection.exists_orthogonal (K := K) (f.symm v) with ⟨w, hwK, hw⟩
    refine ⟨f w, Submodule.mem_map_of_mem hwK, Set.forall_mem_image.2 fun u hu ↦ ?_⟩
    erw [← f.symm.inner_map_map, f.symm_apply_apply, map_sub, f.symm_apply_apply, hw u hu]

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