Documentation

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.

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) :

A family with at most one point is affinely independent.

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.

@[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

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.

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.

@[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

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.

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.

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.

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.

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.

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.

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.

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.

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₂

theorem AffineIndependent.affineCombination_eq_iff_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) {w₁ w₂ : ι → k} {s : Finset ι} (hw₁ : ∑ i ∈ s, w₁ i = 1) (hw₂ : ∑ i ∈ s, w₂ i = 1) :

(Finset.affineCombination k s p) w₁ = (Finset.affineCombination k s p) w₂ ↔ ∀ i ∈ s, w₁ i = w₂ i

Given an affinely independent family of points, two affine combinations (with sum of weights 1) are equal if and only if their weights are pointwise equal.

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.

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.

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.

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.

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

theorem AffineIndependent.comm_left {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ p₂ p₃ : P} (h : AffineIndependent k ![p₁, p₂, p₃]) :

AffineIndependent k ![p₂, p₁, p₃]

Swapping the first two points preserves affine independence.

theorem AffineIndependent.comm_right {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ p₂ p₃ : P} (h : AffineIndependent k ![p₁, p₂, p₃]) :

AffineIndependent k ![p₁, p₃, p₂]

Swapping the last two points preserves affine independence.

theorem AffineIndependent.reverse_of_three {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ p₂ p₃ : P} (h : AffineIndependent k ![p₁, p₂, p₃]) :

AffineIndependent k ![p₃, p₂, p₁]

Reversing the order of three points preserves affine independence.

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.

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) :

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

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.

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₁

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₁

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)) :

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.

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.

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.

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.

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.

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.

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.

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.

@[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.

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.

theorem AffineIndependent.injective_affineSpan_image {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 fun (s : Set ι) => affineSpan k (p '' s)

theorem AffineIndependent.vectorSpan_image_eq_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) {s₁ s₂ : Set ι} :

vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂) ↔ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton

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

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.

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

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

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

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

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.

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.

theorem AffineIndependent.affineCombination_eq_lineMap_iff_weight_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} (ha : 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) (c : k) :

(Finset.affineCombination k s p) w = (AffineMap.lineMap ((Finset.affineCombination k s p) w₁) ((Finset.affineCombination k s p) w₂)) c ↔ ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i)) c

Given an affinely independent family of points, an affine combination (with sum of weights 1) equals the line map of two affine combination points if and only if its weights are given pointwise by the line map of the corresponding weights.

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.

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

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.

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})) :

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.

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.

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.

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.

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.

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.