mathlib

ea9bf31e - refactor(analysis/normed_space/real_inner_product,geometry/euclidean): orthogonal projection hypotheses (#3952)

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.