Commit 2021-10-21 15:43 9c240b58

feat(analysis/inner_product_space): define orthogonal_family of subspaces (#9718) Define orthogonal_family on V : ι → submodule 𝕜 E to mean that any two vectors from distinct subspaces are orthogonal. Prove that an orthogonal family of subspaces is complete_lattice.independent. Also prove that in finite dimension an orthogonal family V satisifies direct_sum.submodule_is_internal (i.e., it provides an internal direct sum decomposition of E) if and only if their joint orthogonal complement is trivial, (supr V)ᗮ = ⊥, and that in this case, the identification of E with the direct sum of V is an isometry.