mathlib

b875cbb7 - feat(linear_algebra/affine_space/affine_subspace): `⊥ < affine_span k s ↔ s.nonempty` (#18170)

feat(linear_algebra/affine_space/affine_subspace): `⊥ < affine_span k s ↔ s.nonempty` (#18170) Two simple corollaries. Also make `s : set P` implicit in the existing lemmas as it can be inferred from the rewrite.