Commit 2025-12-05 16:31 169d847d

feat(LinearAlgebra/AffineSpace/Independent): injectivity of spans of images (#31979) Add the lemma

lemma AffineIndependent.injective_affineSpan_image [Nontrivial k] {p : ι → P}
    (ha : AffineIndependent k p) : Injective fun (s : Set ι) ↦ affineSpan k (p '' s) := by

which is straightforward given existing lemmas, and the corresponding vectorSpan lemma

lemma AffineIndependent.vectorSpan_image_eq_iff [Nontrivial k] {p : ι → P}
    (ha : AffineIndependent k p) {s₁ s₂ : Set ι} :
    vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂) ↔
      s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton := by

(feel free to golf).