Commit 2023-02-22 12:50 b875cbb7
View on Github →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.