mathlib3

9c240b58 - feat(analysis/inner_product_space): define `orthogonal_family` of subspaces (#9718)

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.