ThmDex – An index of mathematical definitions, results, and conjectures.
Result R1396 on D36: Orthogonal projection operator
Image elements of orthogonal projection and coprojection are orthogonal