# Affine independence #

This file defines affinely independent families of points.

## Main definitions #

- `AffineIndependent` defines affinely independent families of points as those where no nontrivial weighted subtraction is `0`. This is proved equivalent to two other formulations: linear independence of the results of subtracting a base point in the family from the other points in the family, or any equal affine combinations having the same weights.

## References #

- https://en.wikipedia.org/wiki/Affine_space

source
def AffineIndependent (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ι → P) :
Prop

An indexed family is said to be affinely independent if no nontrivial weighted subtractions (where the sum of weights is 0) are 0.

Equations

- AffineIndependent k p = ∀ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 → (s.weightedVSub p) w = 0 → ∀ i ∈ s, w i = 0

Instances For

source
theorem affineIndependent_def (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ι → P) :
AffineIndependent k p ↔ ∀ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 → (s.weightedVSub p) w = 0 → ∀ i ∈ s, w i = 0

The definition of `AffineIndependent`.

source
theorem affineIndependent_of_subsingleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Subsingleton ι] (p : ι → P) :
AffineIndependent k p

A family with at most one point is affinely independent.

source
theorem affineIndependent_iff_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Fintype ι] (p : ι → P) :
AffineIndependent k p ↔ ∀ (w : ι → k), ∑ i : ι, w i = 0 → (Finset.univ.weightedVSub p) w = 0 → ∀ (i : ι), w i = 0

A family indexed by a `Fintype` is affinely independent if and only if no nontrivial weighted subtractions over `Finset.univ` (where the sum of the weights is 0) are 0.

source
@[simp]
theorem affineIndependent_vadd (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} {v : V} :
AffineIndependent k (v +ᵥ p) ↔ AffineIndependent k p
source
theorem AffineIndependent.of_vadd (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} {v : V} :
AffineIndependent k (v +ᵥ p) → AffineIndependent k p

Alias of the forward direction of `affineIndependent_vadd`.

source
theorem AffineIndependent.vadd (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} {v : V} :
AffineIndependent k p → AffineIndependent k (v +ᵥ p)

Alias of the reverse direction of `affineIndependent_vadd`.

source
@[simp]
theorem affineIndependent_smul (k : Type u_1) {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {ι : Type u_4} {G : Type u_5} [Group G] [DistribMulAction G V] [SMulCommClass G k V] {p : ι → V} {a : G} :
AffineIndependent k (a • p) ↔ AffineIndependent k p
source
theorem AffineIndependent.of_smul (k : Type u_1) {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {ι : Type u_4} {G : Type u_5} [Group G] [DistribMulAction G V] [SMulCommClass G k V] {p : ι → V} {a : G} :
AffineIndependent k (a • p) → AffineIndependent k p

Alias of the forward direction of `affineIndependent_smul`.

source
theorem AffineIndependent.smul (k : Type u_1) {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {ι : Type u_4} {G : Type u_5} [Group G] [DistribMulAction G V] [SMulCommClass G k V] {p : ι → V} {a : G} :
AffineIndependent k p → AffineIndependent k (a • p)

Alias of the reverse direction of `affineIndependent_smul`.

source
theorem affineIndependent_iff_linearIndependent_vsub (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ι → P) (i1 : ι) :
AffineIndependent k p ↔ LinearIndependent k fun (i : { x : ι // x ≠ i1 }) => p ↑i -ᵥ p i1

A family is affinely independent if and only if the differences from a base point in that family are linearly independent.

source
theorem affineIndependent_set_iff_linearIndependent_vsub (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p₁ : P} (hp₁ : p₁ ∈ s) :
(AffineIndependent k fun (p : ↑s) => ↑p) ↔ LinearIndependent k fun (v : ↑((fun (p : P) => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v

A set is affinely independent if and only if the differences from a base point in that set are linearly independent.

source
theorem linearIndependent_set_iff_affineIndependent_vadd_union_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set V} (hs : ∀ v ∈ s, v ≠ 0) (p₁ : P) :
(LinearIndependent k fun (v : ↑s) => ↑v) ↔ AffineIndependent k fun (p : ↑({p₁} ∪ (fun (v : V) => v +ᵥ p₁) '' s)) => ↑p

A set of nonzero vectors is linearly independent if and only if, given a point `p₁`, the vectors added to `p₁` and `p₁` itself are affinely independent.

source
theorem affineIndependent_iff_indicator_eq_of_affineCombination_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ι → P) :
AffineIndependent k p ↔ ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k), ∑ i ∈ s1, w1 i = 1 → ∑ i ∈ s2, w2 i = 1 → (Finset.affineCombination k s1 p) w1 = (Finset.affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2

A family is affinely independent if and only if any affine combinations (with sum of weights 1) that evaluate to the same point have equal `Set.indicator`.

source
theorem affineIndependent_iff_eq_of_fintype_affineCombination_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Fintype ι] (p : ι → P) :
AffineIndependent k p ↔ ∀ (w1 w2 : ι → k), ∑ i : ι, w1 i = 1 → ∑ i : ι, w2 i = 1 → (Finset.affineCombination k Finset.univ p) w1 = (Finset.affineCombination k Finset.univ p) w2 → w1 = w2

A finite family is affinely independent if and only if any affine combinations (with sum of weights 1) that evaluate to the same point are equal.

source
theorem AffineIndependent.units_lineMap {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (hp : AffineIndependent k p) (j : ι) (w : ι → k ˣ) :
AffineIndependent k fun (i : ι) => (AffineMap.lineMap (p j) (p i)) ↑(w i)

If we single out one member of an affine-independent family of points and affinely transport all others along the line joining them to this member, the resulting new family of points is affine- independent.

This is the affine version of `LinearIndependent.units_smul`.

source
theorem AffineIndependent.indicator_eq_of_affineCombination_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (ha : AffineIndependent k p) (s₁ s₂ : Finset ι) (w₁ w₂ : ι → k) (hw₁ : ∑ i ∈ s₁, w₁ i = 1) (hw₂ : ∑ i ∈ s₂, w₂ i = 1) (h : (Finset.affineCombination k s₁ p) w₁ = (Finset.affineCombination k s₂ p) w₂) :
(↑s₁).indicator w₁ = (↑s₂).indicator w₂
source
theorem AffineIndependent.injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) :
Function.Injective p

An affinely independent family is injective, if the underlying ring is nontrivial.

source
theorem AffineIndependent.comp_embedding {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {ι2 : Type u_5} (f : ι2 ↪ ι) {p : ι → P} (ha : AffineIndependent k p) :
AffineIndependent k (p ∘ ⇑f)

If a family is affinely independent, so is any subfamily given by composition of an embedding into index type with the original family.

source
theorem AffineIndependent.subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (ha : AffineIndependent k p) (s : Set ι) :
AffineIndependent k fun (i : ↑s) => p ↑i

If a family is affinely independent, so is any subfamily indexed by a subtype of the index type.

source
theorem AffineIndependent.range {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (ha : AffineIndependent k p) :
AffineIndependent k fun (x : ↑(Set.range p)) => ↑x

If an indexed family of points is affinely independent, so is the corresponding set of points.

source
theorem affineIndependent_equiv {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') {p : ι' → P} :
AffineIndependent k (p ∘ ⇑e) ↔ AffineIndependent k p
source
theorem AffineIndependent.mono {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s t : Set P} (ha : AffineIndependent k fun (x : ↑t) => ↑x) (hs : s ⊆ t) :
AffineIndependent k fun (x : ↑s) => ↑x

If a set of points is affinely independent, so is any subset.

source
theorem AffineIndependent.of_set_of_injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (ha : AffineIndependent k fun (x : ↑(Set.range p)) => ↑x) (hi : Function.Injective p) :
AffineIndependent k p

If the range of an injective indexed family of points is affinely independent, so is that family.

source
theorem AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (ha : AffineIndependent k p) {fs : Finset ι} {w : ι → k} (hw : ∑ i ∈ fs, w i = 1) {s : Set ι} (hm : (Finset.affineCombination k fs p) w ∈ affineSpan k (p '' s)) {i : ι} (hifs : i ∈ fs) (his : i ∉ s) :
w i = 0

If an affine combination of affinely independent points lies in the affine span of a subset of those points, all weights outside that subset are zero.

source
theorem AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} {p : ι → P} (ha : AffineIndependent k p) {s₁ : Finset ι} {s₂ : Finset ι₂} {w₁ : ι → k} {w₂ : ι₂ → k} (hw₁ : ∑ i ∈ s₁, w₁ i = 1) (hw₂ : ∑ i ∈ s₂, w₂ i = 1) (e : ι₂ ↪ ι) (h : (Finset.affineCombination k s₂ (p ∘ ⇑e)) w₂ = (Finset.affineCombination k s₁ p) w₁) :
(↑(Finset.map e s₂)).indicator (Function.extend (⇑e) w₂ 0) = (↑s₁).indicator w₁
source
theorem AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq_of_fintype {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Fintype ι] {ι₂ : Type u_5} [Fintype ι₂] {p : ι → P} (ha : AffineIndependent k p) {w₁ : ι → k} {w₂ : ι₂ → k} (hw₁ : ∑ i : ι, w₁ i = 1) (hw₂ : ∑ i : ι₂, w₂ i = 1) (e : ι₂ ↪ ι) (h : (Finset.affineCombination k Finset.univ (p ∘ ⇑e)) w₂ = (Finset.affineCombination k Finset.univ p) w₁) :
(Set.range ⇑e).indicator (Function.extend (⇑e) w₂ 0) = w₁
source
theorem AffineIndependent.of_comp {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {p : ι → P} (f : P →ᵃ[k] P₂) (hai : AffineIndependent k (⇑f ∘ p)) :
AffineIndependent k p

If the image of a family of points in affine space under an affine transformation is affine- independent, then the original family of points is also affine-independent.

source
theorem AffineIndependent.map' {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {p : ι → P} (hai : AffineIndependent k p) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) :
AffineIndependent k (⇑f ∘ p)

The image of a family of points in affine space, under an injective affine transformation, is affine-independent.

source
theorem AffineMap.affineIndependent_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {p : ι → P} (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) :
AffineIndependent k (⇑f ∘ p) ↔ AffineIndependent k p

Injective affine maps preserve affine independence.

source
theorem AffineEquiv.affineIndependent_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {p : ι → P} (e : P ≃ᵃ[k] P₂) :
AffineIndependent k (⇑e ∘ p) ↔ AffineIndependent k p

Affine equivalences preserve affine independence of families of points.

source
theorem AffineEquiv.affineIndependent_set_of_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {V₂ : Type u_5} {P₂ : Type u_6} [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {s : Set P} (e : P ≃ᵃ[k] P₂) :
AffineIndependent k Subtype.val ↔ AffineIndependent k Subtype.val

Affine equivalences preserve affine independence of subsets.

source
theorem AffineIndependent.inf_affineSpan_eq_affineSpan_inter {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) (s₁ s₂ : Set ι) :
affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂) = affineSpan k (p '' (s₁ ∩ s₂))

If a family is affinely independent, the infimum of the affine spans of points indexed by two subsets equals the affine span of points indexed by the intersection of those subsets, if the underlying ring is nontrivial.

source
theorem AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) {s1 s2 : Set ι} {p0 : P} (hp0s1 : p0 ∈ affineSpan k (p '' s1)) (hp0s2 : p0 ∈ affineSpan k (p '' s2)) :
∃ (i : ι), i ∈ s1 ∩ s2

If a family is affinely independent, and the spans of points indexed by two subsets of the index type have a point in common, those subsets of the index type have an element in common, if the underlying ring is nontrivial.

source
theorem AffineIndependent.affineSpan_disjoint_of_disjoint {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) {s1 s2 : Set ι} (hd : Disjoint s1 s2) :
Disjoint ↑(affineSpan k (p '' s1)) ↑(affineSpan k (p '' s2))

If a family is affinely independent, the spans of points indexed by disjoint subsets of the index type are disjoint, if the underlying ring is nontrivial.

source
@[simp]
theorem AffineIndependent.mem_affineSpan_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) (i : ι) (s : Set ι) :
p i ∈ affineSpan k (p '' s) ↔ i ∈ s

If a family is affinely independent, a point in the family is in the span of some of the points given by a subset of the index type if and only if that point's index is in the subset, if the underlying ring is nontrivial.

source
theorem AffineIndependent.notMem_affineSpan_diff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) (i : ι) (s : Set ι) :
p i ∉ affineSpan k (p '' (s \ {i}))

If a family is affinely independent, a point in the family is not in the affine span of the other points, if the underlying ring is nontrivial.

source
@[deprecated AffineIndependent.notMem_affineSpan_diff (since := "2025-05-23")]
theorem AffineIndependent.not_mem_affineSpan_diff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) (i : ι) (s : Set ι) :
p i ∉ affineSpan k (p '' (s \ {i}))

Alias of `AffineIndependent.notMem_affineSpan_diff`.

If a family is affinely independent, a point in the family is not in the affine span of the other points, if the underlying ring is nontrivial.

source
theorem exists_nontrivial_relation_sum_zero_of_not_affine_ind {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {t : Finset V} (h : ¬AffineIndependent k Subtype.val) :
∃ (f : V → k), ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0
source
theorem affineIndependent_iff {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {ι : Type u_5} {p : ι → V} :
AffineIndependent k p ↔ ∀ (s : Finset ι) (w : ι → k), s.sum w = 0 → ∑ e ∈ s, w e • p e = 0 → ∀ e ∈ s, w e = 0

Viewing a module as an affine space modelled on itself, we can characterise affine independence in terms of linear combinations.

source
theorem AffineIndependent.eq_zero_of_sum_eq_zero {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {ι : Type u_4} {s : Finset ι} {w : ι → k} {p : ι → V} (hp : AffineIndependent k p) (hw₀ : ∑ i ∈ s, w i = 0) (hw₁ : ∑ i ∈ s, w i • p i = 0) (i : ι) :
i ∈ s → w i = 0
source
theorem AffineIndependent.eq_of_sum_eq_sum {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {ι : Type u_4} {s : Finset ι} {w₁ w₂ : ι → k} {p : ι → V} (hp : AffineIndependent k p) (hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i) (hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i) (i : ι) :
i ∈ s → w₁ i = w₂ i
source
theorem AffineIndependent.eq_zero_of_sum_eq_zero_subtype {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {s : Finset V} (hp : AffineIndependent k Subtype.val) {w : V → k} (hw₀ : ∑ x ∈ s, w x = 0) (hw₁ : ∑ x ∈ s, w x • x = 0) (x : V) :
x ∈ s → w x = 0
source
theorem AffineIndependent.eq_of_sum_eq_sum_subtype {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {s : Finset V} (hp : AffineIndependent k Subtype.val) {w₁ w₂ : V → k} (hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i) (hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i) (i : V) :
i ∈ s → w₁ i = w₂ i
source
theorem weightedVSub_mem_vectorSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (h : AffineIndependent k p) {w w₁ w₂ : ι → k} {s : Finset ι} (hw : ∑ i ∈ s, w i = 0) (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) :
(s.weightedVSub p) w ∈ vectorSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂} ↔ ∃ (r : k), ∀ i ∈ s, w i = r * (w₁ i - w₂ i)

Given an affinely independent family of points, a weighted subtraction lies in the `vectorSpan` of two points given as affine combinations if and only if it is a weighted subtraction with weights a multiple of the difference between the weights of the two points.

source
theorem affineCombination_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (h : AffineIndependent k p) {w w₁ w₂ : ι → k} {s : Finset ι} :
∑ i ∈ s, w i = 1 → ∀ (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1), (Finset.affineCombination k s p) w ∈ affineSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂} ↔ ∃ (r : k), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i

Given an affinely independent family of points, an affine combination lies in the span of two points given as affine combinations if and only if it is an affine combination with weights those of one point plus a multiple of the difference between the weights of the two points.

source
theorem exists_subset_affineIndependent_affineSpan_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} (h : AffineIndependent k fun (p : ↑s) => ↑p) :
∃ (t : Set P), s ⊆ t ∧ (AffineIndependent k fun (p : ↑t) => ↑p) ∧ affineSpan k t = ⊤

An affinely independent set of points can be extended to such a set that spans the whole space.

source
theorem exists_affineIndependent (k : Type u_1) (V : Type u_2) {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) :
∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k Subtype.val
source
theorem affineIndependent_of_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ p₂ : P} (h : p₁ ≠ p₂) :
AffineIndependent k ![p₁, p₂]

Two different points are affinely independent.

source
theorem AffineIndependent.affineIndependent_of_notMem_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} {i : ι} (ha : AffineIndependent k fun (x : { y : ι // y ≠ i }) => p ↑x) (hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})) :
AffineIndependent k p

If all but one point of a family are affinely independent, and that point does not lie in the affine span of that family, the family is affinely independent.

source
@[deprecated AffineIndependent.affineIndependent_of_notMem_span (since := "2025-05-23")]
theorem AffineIndependent.affineIndependent_of_not_mem_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} {i : ι} (ha : AffineIndependent k fun (x : { y : ι // y ≠ i }) => p ↑x) (hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})) :
AffineIndependent k p

Alias of `AffineIndependent.affineIndependent_of_notMem_span`.

If all but one point of a family are affinely independent, and that point does not lie in the affine span of that family, the family is affinely independent.

source
theorem affineIndependent_of_ne_of_mem_of_mem_of_notMem {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ p₃ : P} (hp₁p₂ : p₁ ≠ p₂) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∉ s) :
AffineIndependent k ![p₁, p₂, p₃]

If distinct points `p₁` and `p₂` lie in `s` but `p₃` does not, the three points are affinely independent.

source
@[deprecated affineIndependent_of_ne_of_mem_of_mem_of_notMem (since := "2025-05-23")]
theorem affineIndependent_of_ne_of_mem_of_mem_of_not_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ p₃ : P} (hp₁p₂ : p₁ ≠ p₂) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∉ s) :
AffineIndependent k ![p₁, p₂, p₃]

Alias of `affineIndependent_of_ne_of_mem_of_mem_of_notMem`.

If distinct points `p₁` and `p₂` lie in `s` but `p₃` does not, the three points are affinely independent.

source
theorem affineIndependent_of_ne_of_mem_of_notMem_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ p₃ : P} (hp₁p₃ : p₁ ≠ p₃) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∉ s) (hp₃ : p₃ ∈ s) :
AffineIndependent k ![p₁, p₂, p₃]

If distinct points `p₁` and `p₃` lie in `s` but `p₂` does not, the three points are affinely independent.

source
@[deprecated affineIndependent_of_ne_of_mem_of_notMem_of_mem (since := "2025-05-23")]
theorem affineIndependent_of_ne_of_mem_of_not_mem_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ p₃ : P} (hp₁p₃ : p₁ ≠ p₃) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∉ s) (hp₃ : p₃ ∈ s) :
AffineIndependent k ![p₁, p₂, p₃]

Alias of `affineIndependent_of_ne_of_mem_of_notMem_of_mem`.

If distinct points `p₁` and `p₃` lie in `s` but `p₂` does not, the three points are affinely independent.

source
theorem affineIndependent_of_ne_of_notMem_of_mem_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ p₃ : P} (hp₂p₃ : p₂ ≠ p₃) (hp₁ : p₁ ∉ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) :
AffineIndependent k ![p₁, p₂, p₃]

If distinct points `p₂` and `p₃` lie in `s` but `p₁` does not, the three points are affinely independent.

source
@[deprecated affineIndependent_of_ne_of_notMem_of_mem_of_mem (since := "2025-05-23")]
theorem affineIndependent_of_ne_of_not_mem_of_mem_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ p₃ : P} (hp₂p₃ : p₂ ≠ p₃) (hp₁ : p₁ ∉ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) :
AffineIndependent k ![p₁, p₂, p₃]

Alias of `affineIndependent_of_ne_of_notMem_of_mem_of_mem`.

If distinct points `p₂` and `p₃` lie in `s` but `p₁` does not, the three points are affinely independent.

source
theorem AffineIndependent.affineIndependent_update_of_notMem_affineSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} [DecidableEq ι] {p : ι → P} (ha : AffineIndependent k p) {i : ι} {p₀ : P} (hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})) :
AffineIndependent k (Function.update p i p₀)

If a family is affinely independent, we update any one point with a new point does not lie in the affine span of that family, the new family is affinely independent.

source
theorem sign_eq_of_affineCombination_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (h : AffineIndependent k p) {w w₁ w₂ : ι → k} {s : Finset ι} (hw : ∑ i ∈ s, w i = 1) (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) (hs : (Finset.affineCombination k s p) w ∈ affineSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂}) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hi0 : w₁ i = 0) (hj0 : w₁ j = 0) (hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)) :
SignType.sign (w i) = SignType.sign (w j)

Given an affinely independent family of points, suppose that an affine combination lies in the span of two points given as affine combinations, and suppose that, for two indices, the coefficients in the first point in the span are zero and those in the second point in the span have the same sign. Then the coefficients in the combination lying in the span have the same sign.

source
theorem sign_eq_of_affineCombination_mem_affineSpan_single_lineMap {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [LinearOrder k] [IsStrictOrderedRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} {p : ι → P} (h : AffineIndependent k p) {w : ι → k} {s : Finset ι} (hw : ∑ i ∈ s, w i = 1) {i₁ i₂ i₃ : ι} (h₁ : i₁ ∈ s) (h₂ : i₂ ∈ s) (h₃ : i₃ ∈ s) (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {c : k} (hc0 : 0 < c) (hc1 : c < 1) (hs : (Finset.affineCombination k s p) w ∈ affineSpan k {p i₁, (AffineMap.lineMap (p i₂) (p i₃)) c}) :
SignType.sign (w i₂) = SignType.sign (w i₃)

Given an affinely independent family of points, suppose that an affine combination lies in the span of one point of that family and a combination of another two points of that family given by `lineMap` with coefficient between 0 and 1. Then the coefficients of those two points in the combination lying in the span have the same sign.