Commit 2020-08-27 06:25 ea9bf31e

refactor(analysis/normed_space/real_inner_product,geometry/euclidean): orthogonal projection hypotheses (#3952) As advised by Patrick in #3932, define orthogonal_projection (for both real inner product spaces and Euclidean affine spaces) without taking hypotheses of the subspace being nonempty and complete, defaulting to the identity map if those conditions are not satisfied, so making orthogonal_projection more convenient to use with those properties only being needed on lemmas but not simply to refer to the orthogonal projection at all. The hypotheses are removed from lemmas that don't need them because they are still true with the identity map. Some nonempty hypotheses are also removed where they follow from another hypothesis that gives a point or a nonempty set of points in the subspace. The unbundled orthogonal_projection_fn that's used only to prove properties needed to define a bundled linear or affine map still takes the original hypotheses, then a bundled map taking those hypotheses is defined under a new name, then that map is used to define plain orthogonal_projection which does not take any of those hypotheses and is the version expected to be used in all lemmas after it has been defined.