Commit 2022-08-16 16:11 c62c909c

View on Github →

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.

Estimated changes

Modified src/linear_algebra/projective_space/subspace.lean

added theorem projectivization.subspace.mem_span

added theorem projectivization.subspace.monotone_span

added theorem projectivization.subspace.span_Union

modified theorem projectivization.subspace.span_coe

added theorem projectivization.subspace.span_empty

added theorem projectivization.subspace.span_eq_Inf

added theorem projectivization.subspace.span_eq_of_le

added theorem projectivization.subspace.span_eq_span_iff

added theorem projectivization.subspace.span_le_subspace_iff

added theorem projectivization.subspace.span_sup

added theorem projectivization.subspace.span_union

added theorem projectivization.subspace.span_univ

added theorem projectivization.subspace.subset_span_trans

added theorem projectivization.subspace.sup_span