mathlib3

c62c909c - feat(linear_algebra/projective_space/subspace): adds lemmas about the span operation and supremums of collections of subspaces (#15596)

feat(linear_algebra/projective_space/subspace): adds lemmas about the span operation and supremums of collections of subspaces (#15596) This PR adds lemmas relating the span operation to the order relations between subsets and subspaces, and adds lemmas about computing the supremum of a collection of subspaces using the span operation.