instHasOrthogonalProjectionOrthogonal

English

If K has an orthogonal projection, then the orthogonal complement K^⊥ also has an orthogonal projection.

Русский

Если K имеет ортогональную проекцию, то и ортогональное дополнение K^⊥ имеет ортогональную проекцию.

LaTeX

$$Kᗮ.HasOrthogonalProjection$$

Lean4

instance [K.HasOrthogonalProjection] : Kᗮ.HasOrthogonalProjection where
  exists_orthogonal
    v := by
    rcases HasOrthogonalProjection.exists_orthogonal (K := K) v with ⟨w, hwK, hw⟩
    refine ⟨_, hw, ?_⟩
    rw [sub_sub_cancel]
    exact K.le_orthogonal_orthogonal hwK

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