mathlib

0e86ecbb - feat(linear_algebra/affine_space/affine_subspace): `affine_span_pair` inequality lemmas (#17636)

feat(linear_algebra/affine_space/affine_subspace): `affine_span_pair` inequality lemmas (#17636) Add some lemmas giving conditions for the affine span of two points to be contained in an affine subspace (in particular, the span of another two points, one point the same between the pairs), in terms of individual points lying in that subspace. These are easy consequences of existing lemmas, but convenient when working with spans of two points.