doc-next-gen

Mathlib.LinearAlgebra.AffineSpace.Independent

Module docstring

{"# 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. A bundled type Simplex is provided for finite affinely independent families of points, with an abbreviation Triangle for the case of three points.

References

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

"}

AffineIndependent definition
(p : ι → P) : Prop
Full source 
/-- An indexed family is said to be affinely independent if no
nontrivial weighted subtractions (where the sum of weights is 0) are
0. -/
def AffineIndependent (p : ι → P) : Prop :=
  ∀ (s : Finset ι) (w : ι → k),
    ∑ i ∈ s, w i = 0 → s.weightedVSub p w = (0 : V) → ∀ i ∈ s, w i = 0
Affinely independent family of points
Informal description
A family of points \( p : \iota \to P \) in an affine space is called *affinely independent* if for any finite subset \( s \) of \( \iota \) and any weights \( w : \iota \to k \) summing to zero, the weighted subtraction \( \sum_{i \in s} w_i (p_i - p_j) = 0 \) (for some fixed \( j \in s \)) implies that all weights \( w_i \) are zero.
affineIndependent_def theorem
(p : ι → P) : AffineIndependent k p ↔ ∀ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 → s.weightedVSub p w = (0 : V) → ∀ i ∈ s, w i = 0
Full source 
/-- The definition of `AffineIndependent`. -/
theorem affineIndependent_def (p : ι → P) :
    AffineIndependentAffineIndependent k p ↔
      ∀ (s : Finset ι) (w : ι → k),
        ∑ i ∈ s, w i = 0 → s.weightedVSub p w = (0 : V) → ∀ i ∈ s, w i = 0 :=
  Iff.rfl
Characterization of Affinely Independent Points via Weighted Subtractions
Informal description
A family of points $\{p_i\}_{i \in \iota}$ in an affine space over a field $k$ is *affinely independent* if and only if for every finite subset $s \subseteq \iota$ and every weight function $w : \iota \to k$ such that $\sum_{i \in s} w_i = 0$, the condition $\sum_{i \in s} w_i (p_i - p_j) = 0$ (for any fixed $j \in s$) implies that $w_i = 0$ for all $i \in s$.
affineIndependent_of_subsingleton theorem
[Subsingleton ι] (p : ι → P) : AffineIndependent k p
Full source 
/-- A family with at most one point is affinely independent. -/
theorem affineIndependent_of_subsingleton [Subsingleton ι] (p : ι → P) : AffineIndependent k p :=
  fun _ _ h _ i hi => Fintype.eq_of_subsingleton_of_sum_eq h i hi
Affine Independence of Singleton or Empty Families
Informal description
For any type $\iota$ with at most one element (i.e., a subsingleton) and any family of points $p : \iota \to P$ in an affine space, the family $p$ is affinely independent.
affineIndependent_iff_of_fintype theorem
[Fintype ι] (p : ι → P) : AffineIndependent k p ↔ ∀ w : ι → k, ∑ i, w i = 0 → Finset.univ.weightedVSub p w = (0 : V) → ∀ i, w i = 0
Full source 
/-- 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. -/
theorem affineIndependent_iff_of_fintype [Fintype ι] (p : ι → P) :
    AffineIndependentAffineIndependent k p ↔
      ∀ w : ι → k, ∑ i, w i = 0 → Finset.univ.weightedVSub p w = (0 : V) → ∀ i, w i = 0 := by
  constructor
  · exact fun h w hw hs i => h Finset.univ w hw hs i (Finset.mem_univ _)
  · intro h s w hw hs i hi
    rw [Finset.weightedVSub_indicator_subset _ _ (Finset.subset_univ s)] at hs
    rw [← Finset.sum_indicator_subset _ (Finset.subset_univ s)] at hw
    replace h := h ((↑s : Set ι).indicator w) hw hs i
    simpa [hi] using h
Characterization of Affinely Independent Points via Weighted Subtractions over Finite Types
Informal description
Let $\iota$ be a finite type and $p : \iota \to P$ be a family of points in an affine space over a field $k$. The family $p$ is affinely independent if and only if for every weight function $w : \iota \to k$ such that $\sum_{i \in \iota} w_i = 0$, the condition $\sum_{i \in \iota} w_i (p_i - p_j) = 0$ (for any fixed $j \in \iota$) implies that $w_i = 0$ for all $i \in \iota$.
affineIndependent_vadd theorem
{p : ι → P} {v : V} : AffineIndependent k (v +ᵥ p) ↔ AffineIndependent k p
Full source 
@[simp] lemma affineIndependent_vadd {p : ι → P} {v : V} :
    AffineIndependentAffineIndependent k (v +ᵥ p) ↔ AffineIndependent k p := by
  simp +contextual [AffineIndependent, weightedVSub_vadd]
Affine independence is preserved under translation by a vector
Informal description
Let $V$ be a vector space over a field $k$ and $P$ an affine space over $V$. For any family of points $p : \iota \to P$ and any vector $v \in V$, the family $(v + p_i)_{i \in \iota}$ is affinely independent if and only if the original family $(p_i)_{i \in \iota}$ is affinely independent.
affineIndependent_smul theorem
{G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V] {p : ι → V} {a : G} : AffineIndependent k (a • p) ↔ AffineIndependent k p
Full source 
@[simp] lemma affineIndependent_smul {G : Type*} [Group G] [DistribMulAction G V]
    [SMulCommClass G k V] {p : ι → V} {a : G} :
    AffineIndependentAffineIndependent k (a • p) ↔ AffineIndependent k p := by
  simp +contextual [AffineIndependent, weightedVSub_smul,
    ← smul_comm (α := V) a, ← smul_sum, smul_eq_zero_iff_eq]
Affine Independence under Group Action: $a \cdot p$ is affinely independent if and only if $p$ is
Informal description
Let $G$ be a group acting distributively on a vector space $V$ over a field $k$, with the action commuting with scalar multiplication. For any family of points $p : \iota \to V$ and any element $a \in G$, the family $a \cdot p$ is affinely independent if and only if the original family $p$ is affinely independent.
affineIndependent_iff_linearIndependent_vsub theorem
(p : ι → P) (i1 : ι) : AffineIndependent k p ↔ LinearIndependent k fun i : { x // x ≠ i1 } => (p i -ᵥ p i1 : V)
Full source 
/-- A family is affinely independent if and only if the differences
from a base point in that family are linearly independent. -/
theorem affineIndependent_iff_linearIndependent_vsub (p : ι → P) (i1 : ι) :
    AffineIndependentAffineIndependent k p ↔ LinearIndependent k fun i : { x // x ≠ i1 } => (p i -ᵥ p i1 : V) := by
  classical
    constructor
    · intro h
      rw [linearIndependent_iff']
      intro s g hg i hi
      set f : ι → k := fun x => if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩ with hfdef
      let s2 : Finset ι := insert i1 (s.map (Embedding.subtype _))
      have hfg : ∀ x : { x // x ≠ i1 }, g x = f x := by
        intro x
        rw [hfdef]
        dsimp only
        rw [dif_neg x.property, Subtype.coe_eta]
      rw [hfg]
      have hf : ∑ ι ∈ s2, f ι = 0 := by
        rw [Finset.sum_insert
            (Finset.not_mem_map_subtype_of_not_property s (Classical.not_not.2 rfl)),
          Finset.sum_subtype_map_embedding fun x _ => (hfg x).symm]
        rw [hfdef]
        dsimp only
        rw [dif_pos rfl]
        exact neg_add_cancel _
      have hs2 : s2.weightedVSub p f = (0 : V) := by
        set f2 : ι → V := fun x => f x • (p x -ᵥ p i1) with hf2def
        set g2 : { x // x ≠ i1 } → V := fun x => g x • (p x -ᵥ p i1)
        have hf2g2 : ∀ x : { x // x ≠ i1 }, f2 x = g2 x := by
          simp only [g2, hf2def]
          refine fun x => ?_
          rw [hfg]
        rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s2 f p hf (p i1),
          Finset.weightedVSubOfPoint_insert, Finset.weightedVSubOfPoint_apply,
          Finset.sum_subtype_map_embedding fun x _ => hf2g2 x]
        exact hg
      exact h s2 f hf hs2 i (Finset.mem_insert_of_mem (Finset.mem_map.2 ⟨i, hi, rfl⟩))
    · intro h
      rw [linearIndependent_iff'] at h
      intro s w hw hs i hi
      rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p hw (p i1), ←
        s.weightedVSubOfPoint_erase w p i1, Finset.weightedVSubOfPoint_apply] at hs
      let f : ι → V := fun i => w i • (p i -ᵥ p i1)
      have hs2 : (∑ i ∈ (s.erase i1).subtype fun i => i ≠ i1, f i) = 0 := by
        rw [← hs]
        convert Finset.sum_subtype_of_mem f fun x => Finset.ne_of_mem_erase
      have h2 := h ((s.erase i1).subtype fun i => i ≠ i1) (fun x => w x) hs2
      simp_rw [Finset.mem_subtype] at h2
      have h2b : ∀ i ∈ s, i ≠ i1 → w i = 0 := fun i his hi =>
        h2 ⟨i, hi⟩ (Finset.mem_erase_of_ne_of_mem hi his)
      exact Finset.eq_zero_of_sum_eq_zero hw h2b i hi
Affine Independence via Linear Independence of Difference Vectors
Informal description
A family of points $p : \iota \to P$ in an affine space over a vector space $V$ is affinely independent if and only if, for any fixed index $i_1 \in \iota$, the family of vectors $\{p_i - p_{i_1}\}_{i \in \iota \setminus \{i_1\}}$ is linearly independent in $V$.
affineIndependent_set_iff_linearIndependent_vsub theorem
{s : Set P} {p₁ : P} (hp₁ : p₁ ∈ s) : AffineIndependent k (fun p => p : s → P) ↔ LinearIndependent k (fun v => v : (fun p => (p -ᵥ p₁ : V)) '' (s \ { p₁ }) → V)
Full source 
/-- A set is affinely independent if and only if the differences from
a base point in that set are linearly independent. -/
theorem affineIndependent_set_iff_linearIndependent_vsub {s : Set P} {p₁ : P} (hp₁ : p₁ ∈ s) :
    AffineIndependentAffineIndependent k (fun p => p : s → P) ↔
      LinearIndependent k (fun v => v : (fun p => (p -ᵥ p₁ : V)) '' (s \ {p₁}) → V) := by
  rw [affineIndependent_iff_linearIndependent_vsub k (fun p => p : s → P) ⟨p₁, hp₁⟩]
  constructor
  · intro h
    have hv : ∀ v : (fun p => (p -ᵥ p₁ : V)) '' (s \ {p₁}), (v : V) +ᵥ p₁(v : V) +ᵥ p₁ ∈ s \ {p₁} := fun v =>
      (vsub_left_injective p₁).mem_set_image.1 ((vadd_vsub (v : V) p₁).symm ▸ v.property)
    let f : (fun p : P => (p -ᵥ p₁ : V)) '' (s \ {p₁}) → { x : s // x ≠ ⟨p₁, hp₁⟩ } := fun x =>
      ⟨⟨(x : V) +ᵥ p₁, Set.mem_of_mem_diff (hv x)⟩, fun hx =>
        Set.not_mem_of_mem_diff (hv x) (Subtype.ext_iff.1 hx)⟩
    convert h.comp f fun x1 x2 hx =>
        Subtype.ext (vadd_right_cancel p₁ (Subtype.ext_iff.1 (Subtype.ext_iff.1 hx)))
    ext v
    exact (vadd_vsub (v : V) p₁).symm
  · intro h
    let f : { x : s // x ≠ ⟨p₁, hp₁⟩ } → (fun p : P => (p -ᵥ p₁ : V)) '' (s \ {p₁}) := fun x =>
      ⟨((x : s) : P) -ᵥ p₁, ⟨x, ⟨⟨(x : s).property, fun hx => x.property (Subtype.ext hx)⟩, rfl⟩⟩⟩
    convert h.comp f fun x1 x2 hx =>
        Subtype.ext (Subtype.ext (vsub_left_cancel (Subtype.ext_iff.1 hx)))
Affine Independence of a Set via Linear Independence of Difference Vectors
Informal description
Let $s$ be a set of points in an affine space over a vector space $V$, and let $p_1 \in s$ be a fixed point. The family of points in $s$ is affinely independent if and only if the set of difference vectors $\{p - p_1 \mid p \in s \setminus \{p_1\}\}$ is linearly independent in $V$.
linearIndependent_set_iff_affineIndependent_vadd_union_singleton theorem
{s : Set V} (hs : ∀ v ∈ s, v ≠ (0 : V)) (p₁ : P) : LinearIndependent k (fun v => v : s → V) ↔ AffineIndependent k (fun p => p : ({ p₁ } ∪ (fun v => v +ᵥ p₁) '' s : Set P) → P)
Full source 
/-- 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 linearIndependent_set_iff_affineIndependent_vadd_union_singleton {s : Set V}
    (hs : ∀ v ∈ s, v ≠ (0 : V)) (p₁ : P) : LinearIndependentLinearIndependent k (fun v => v : s → V) ↔
    AffineIndependent k (fun p => p : ({p₁} ∪ (fun v => v +ᵥ p₁) '' s : Set P) → P) := by
  rw [affineIndependent_set_iff_linearIndependent_vsub k
      (Set.mem_union_left _ (Set.mem_singleton p₁))]
  have h : (fun p => (p -ᵥ p₁ : V)) '' (({p₁} ∪ (fun v => v +ᵥ p₁) '' s) \ {p₁}) = s := by
    simp_rw [Set.union_diff_left, Set.image_diff (vsub_left_injective p₁), Set.image_image,
      Set.image_singleton, vsub_self, vadd_vsub, Set.image_id']
    exact Set.diff_singleton_eq_self fun h => hs 0 h rfl
  rw [h]
Linear Independence of Vectors vs. Affine Independence of Translated Points
Informal description
Let $V$ be a vector space over a field $k$, and let $s$ be a subset of $V$ such that every vector in $s$ is nonzero. For any point $p_1$ in an affine space $P$ over $V$, the set $s$ is linearly independent in $V$ if and only if the union of the singleton set $\{p_1\}$ and the set obtained by translating each vector in $s$ by $p_1$ (i.e., $\{v + p_1 \mid v \in s\}$) is affinely independent in $P$.
affineIndependent_iff_indicator_eq_of_affineCombination_eq theorem
(p : ι → P) : AffineIndependent k p ↔ ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k), ∑ i ∈ s1, w1 i = 1 → ∑ i ∈ s2, w2 i = 1 → s1.affineCombination k p w1 = s2.affineCombination k p w2 → Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
Full source 
/-- 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_indicator_eq_of_affineCombination_eq (p : ι → P) :
    AffineIndependentAffineIndependent k p ↔
      ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
        ∑ i ∈ s1, w1 i = 1 →
          ∑ i ∈ s2, w2 i = 1 →
            s1.affineCombination k p w1 = s2.affineCombination k p w2 →
              Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2 := by
  classical
    constructor
    · intro ha s1 s2 w1 w2 hw1 hw2 heq
      ext i
      by_cases hi : i ∈ s1 ∪ s2
      · rw [← sub_eq_zero]
        rw [← Finset.sum_indicator_subset w1 (s1.subset_union_left (s₂ := s2))] at hw1
        rw [← Finset.sum_indicator_subset w2 (s1.subset_union_right)] at hw2
        have hws : (∑ i ∈ s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i) = 0 := by
          simp [hw1, hw2]
        rw [Finset.affineCombination_indicator_subset w1 p (s1.subset_union_left (s₂ := s2)),
          Finset.affineCombination_indicator_subset w2 p s1.subset_union_right,
          ← @vsub_eq_zero_iff_eq V, Finset.affineCombination_vsub] at heq
        exact ha (s1 ∪ s2) (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) hws heq i hi
      · rw [← Finset.mem_coe, Finset.coe_union] at hi
        have h₁ : Set.indicator (↑s1) w1 i = 0 := by
          simp only [Set.indicator, Finset.mem_coe, ite_eq_right_iff]
          intro h
          by_contra
          exact (mt (@Set.mem_union_left _ i ↑s1 ↑s2) hi) h
        have h₂ : Set.indicator (↑s2) w2 i = 0 := by
          simp only [Set.indicator, Finset.mem_coe, ite_eq_right_iff]
          intro h
          by_contra
          exact (mt (@Set.mem_union_right _ i ↑s2 ↑s1) hi) h
        simp [h₁, h₂]
    · intro ha s w hw hs i0 hi0
      let w1 : ι → k := Function.update (Function.const ι 0) i0 1
      have hw1 : ∑ i ∈ s, w1 i = 1 := by
        rw [Finset.sum_update_of_mem hi0]
        simp only [Finset.sum_const_zero, add_zero, const_apply]
      have hw1s : s.affineCombination k p w1 = p i0 :=
        s.affineCombination_of_eq_one_of_eq_zero w1 p hi0 (Function.update_self ..)
          fun _ _ hne => Function.update_of_ne hne ..
      let w2 := w + w1
      have hw2 : ∑ i ∈ s, w2 i = 1 := by
        simp_all only [w2, Pi.add_apply, Finset.sum_add_distrib, zero_add]
      have hw2s : s.affineCombination k p w2 = p i0 := by
        simp_all only [w2, ← Finset.weightedVSub_vadd_affineCombination, zero_vadd]
      replace ha := ha s s w2 w1 hw2 hw1 (hw1s.symm ▸ hw2s)
      have hws : w2 i0 - w1 i0 = 0 := by
        rw [← Finset.mem_coe] at hi0
        rw [← Set.indicator_of_mem hi0 w2, ← Set.indicator_of_mem hi0 w1, ha, sub_self]
      simpa [w2] using hws
Affine Independence via Equal Affine Combinations and Indicator Functions
Informal description
A family of points $p \colon \iota \to P$ in an affine space over a ring $k$ is affinely independent if and only if for any two finite subsets $s_1, s_2 \subseteq \iota$ and any weight functions $w_1, w_2 \colon \iota \to k$ satisfying $\sum_{i \in s_1} w_1(i) = 1$ and $\sum_{i \in s_2} w_2(i) = 1$, the equality of affine combinations $s_1.\text{affineCombination}_k p w_1 = s_2.\text{affineCombination}_k p w_2$ implies that the indicator functions of $w_1$ and $w_2$ restricted to $s_1$ and $s_2$ respectively are equal, i.e., $\text{indicator}_{s_1} w_1 = \text{indicator}_{s_2} w_2$.
affineIndependent_iff_eq_of_fintype_affineCombination_eq theorem
[Fintype ι] (p : ι → P) : AffineIndependent k p ↔ ∀ w1 w2 : ι → k, ∑ i, w1 i = 1 → ∑ i, w2 i = 1 → Finset.univ.affineCombination k p w1 = Finset.univ.affineCombination k p w2 → w1 = w2
Full source 
/-- 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_iff_eq_of_fintype_affineCombination_eq [Fintype ι] (p : ι → P) :
    AffineIndependentAffineIndependent k p ↔ ∀ w1 w2 : ι → k, ∑ i, w1 i = 1 → ∑ i, w2 i = 1 →
    Finset.univ.affineCombination k p w1 = Finset.univ.affineCombination k p w2 → w1 = w2 := by
  rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq]
  constructor
  · intro h w1 w2 hw1 hw2 hweq
    simpa only [Set.indicator_univ, Finset.coe_univ] using h _ _ w1 w2 hw1 hw2 hweq
  · intro h s1 s2 w1 w2 hw1 hw2 hweq
    have hw1' : (∑ i, (s1 : Set ι).indicator w1 i) = 1 := by
      rwa [Finset.sum_indicator_subset _ (Finset.subset_univ s1)]
    have hw2' : (∑ i, (s2 : Set ι).indicator w2 i) = 1 := by
      rwa [Finset.sum_indicator_subset _ (Finset.subset_univ s2)]
    rw [Finset.affineCombination_indicator_subset w1 p (Finset.subset_univ s1),
      Finset.affineCombination_indicator_subset w2 p (Finset.subset_univ s2)] at hweq
    exact h _ _ hw1' hw2' hweq
Affine Independence via Unique Weights for Equal Affine Combinations
Informal description
Let $\iota$ be a finite type and $p \colon \iota \to P$ be a family of points in an affine space over a ring $k$. Then $p$ is affinely independent if and only if for any two weight functions $w_1, w_2 \colon \iota \to k$ satisfying $\sum_{i} w_1(i) = 1$ and $\sum_{i} w_2(i) = 1$, the equality of affine combinations $\sum_{i} w_1(i) p_i = \sum_{i} w_2(i) p_i$ implies $w_1 = w_2$.
AffineIndependent.units_lineMap theorem
{p : ι → P} (hp : AffineIndependent k p) (j : ι) (w : ι → Units k) : AffineIndependent k fun i => AffineMap.lineMap (p j) (p i) (w i : k)
Full source 
/-- 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.units_lineMap {p : ι → P} (hp : AffineIndependent k p) (j : ι)
    (w : ι → Units k) : AffineIndependent k fun i => AffineMap.lineMap (p j) (p i) (w i : k) := by
  rw [affineIndependent_iff_linearIndependent_vsub k _ j] at hp ⊢
  simp only [AffineMap.lineMap_vsub_left, AffineMap.coe_const, AffineMap.lineMap_same, const_apply]
  exact hp.units_smul fun i => w i
Affine Independence Preserved Under Unit-Scaled Line Transport
Informal description
Let $k$ be a ring and $P$ an affine space over $k$. Given an affinely independent family of points $p \colon \iota \to P$, a fixed index $j \in \iota$, and a family of units $w \colon \iota \to k^\times$, the family of points obtained by affinely transporting each $p_i$ along the line joining $p_j$ to $p_i$ with scaling factor $w(i)$ is also affinely independent. That is, the family defined by $i \mapsto \text{lineMap}(p_j, p_i)(w(i))$ is affinely independent.
AffineIndependent.indicator_eq_of_affineCombination_eq theorem
{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 : s₁.affineCombination k p w₁ = s₂.affineCombination k p w₂) : Set.indicator (↑s₁) w₁ = Set.indicator (↑s₂) w₂
Full source 
theorem AffineIndependent.indicator_eq_of_affineCombination_eq {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 : s₁.affineCombination k p w₁ = s₂.affineCombination k p w₂) :
    Set.indicator (↑s₁) w₁ = Set.indicator (↑s₂) w₂ :=
  (affineIndependent_iff_indicator_eq_of_affineCombination_eq k p).1 ha s₁ s₂ w₁ w₂ hw₁ hw₂ h
Equal Affine Combinations Imply Equal Indicator Weights for Affinely Independent Points
Informal description
Let $k$ be a ring and $P$ an affine space over $k$. Given an affinely independent family of points $p \colon \iota \to P$, for any two finite subsets $s_1, s_2 \subseteq \iota$ and weight functions $w_1, w_2 \colon \iota \to k$ satisfying $\sum_{i \in s_1} w_1(i) = 1$ and $\sum_{i \in s_2} w_2(i) = 1$, if the affine combinations $s_1.\text{affineCombination}_k p w_1$ and $s_2.\text{affineCombination}_k p w_2$ are equal, then the indicator functions of $w_1$ and $w_2$ restricted to $s_1$ and $s_2$ respectively are equal, i.e., $\text{indicator}_{s_1} w_1 = \text{indicator}_{s_2} w_2$.
AffineIndependent.injective theorem
[Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) : Function.Injective p
Full source 
/-- An affinely independent family is injective, if the underlying
ring is nontrivial. -/
protected theorem AffineIndependent.injective [Nontrivial k] {p : ι → P}
    (ha : AffineIndependent k p) : Function.Injective p := by
  intro i j hij
  rw [affineIndependent_iff_linearIndependent_vsub _ _ j] at ha
  by_contra hij'
  refine ha.ne_zero ⟨i, hij'⟩ (vsub_eq_zero_iff_eq.mpr ?_)
  simp_all only [ne_eq]
Injectivity of Affinely Independent Families over Nontrivial Rings
Informal description
Let $k$ be a nontrivial ring and $P$ an affine space over $k$. For any affinely independent family of points $p \colon \iota \to P$, the function $p$ is injective.
AffineIndependent.comp_embedding theorem
{ι2 : Type*} (f : ι2 ↪ ι) {p : ι → P} (ha : AffineIndependent k p) : AffineIndependent k (p ∘ f)
Full source 
/-- 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.comp_embedding {ι2 : Type*} (f : ι2 ↪ ι) {p : ι → P}
    (ha : AffineIndependent k p) : AffineIndependent k (p ∘ f) := by
  classical
    intro fs w hw hs i0 hi0
    let fs' := fs.map f
    let w' i := if h : ∃ i2, f i2 = i then w h.choose else 0
    have hw' : ∀ i2 : ι2, w' (f i2) = w i2 := by
      intro i2
      have h : ∃ i : ι2, f i = f i2 := ⟨i2, rfl⟩
      have hs : h.choose = i2 := f.injective h.choose_spec
      simp_rw [w', dif_pos h, hs]
    have hw's : ∑ i ∈ fs', w' i = 0 := by
      rw [← hw, Finset.sum_map]
      simp [hw']
    have hs' : fs'.weightedVSub p w' = (0 : V) := by
      rw [← hs, Finset.weightedVSub_map]
      congr with i
      simp_all only [comp_apply, EmbeddingLike.apply_eq_iff_eq, exists_eq, dite_true]
    rw [← ha fs' w' hw's hs' (f i0) ((Finset.mem_map' _).2 hi0), hw']
Affine Independence is Preserved Under Composition with Embedding
Informal description
Let $k$ be a field and $P$ be an affine space over $k$. Given an affinely independent family of points $p : \iota \to P$ and an injective function $f : \iota_2 \hookrightarrow \iota$ (where $\iota_2$ is another index type), the composition $p \circ f : \iota_2 \to P$ is also affinely independent.
AffineIndependent.subtype theorem
{p : ι → P} (ha : AffineIndependent k p) (s : Set ι) : AffineIndependent k fun i : s => p i
Full source 
/-- If a family is affinely independent, so is any subfamily indexed
by a subtype of the index type. -/
protected theorem AffineIndependent.subtype {p : ι → P} (ha : AffineIndependent k p) (s : Set ι) :
    AffineIndependent k fun i : s => p i :=
  ha.comp_embedding (Embedding.subtype _)
Affine Independence is Preserved Under Subset Restriction
Informal description
Let $k$ be a field and $P$ be an affine space over $k$. Given an affinely independent family of points $p : \iota \to P$ and a subset $s \subseteq \iota$, the restricted family of points $\{p_i\}_{i \in s}$ is also affinely independent.
AffineIndependent.range theorem
{p : ι → P} (ha : AffineIndependent k p) : AffineIndependent k (fun x => x : Set.range p → P)
Full source 
/-- If an indexed family of points is affinely independent, so is the
corresponding set of points. -/
protected theorem AffineIndependent.range {p : ι → P} (ha : AffineIndependent k p) :
    AffineIndependent k (fun x => x : Set.range p → P) := by
  let f : Set.range p → ι := fun x => x.property.choose
  have hf : ∀ x, p (f x) = x := fun x => x.property.choose_spec
  let fe : Set.rangeSet.range p ↪ ι := ⟨f, fun x₁ x₂ he => Subtype.ext (hf x₁ ▸ hf x₂ ▸ he ▸ rfl)⟩
  convert ha.comp_embedding fe
  ext
  simp [fe, hf]
Affine Independence of Range of Points
Informal description
Let $k$ be a field and $P$ be an affine space over $k$. If a family of points $p : \iota \to P$ is affinely independent, then the corresponding set of points $\mathrm{range}\, p \subseteq P$ is also affinely independent.
affineIndependent_equiv theorem
{ι' : Type*} (e : ι ≃ ι') {p : ι' → P} : AffineIndependent k (p ∘ e) ↔ AffineIndependent k p
Full source 
theorem affineIndependent_equiv {ι' : Type*} (e : ι ≃ ι') {p : ι' → P} :
    AffineIndependentAffineIndependent k (p ∘ e) ↔ AffineIndependent k p := by
  refine ⟨?_, AffineIndependent.comp_embedding e.toEmbedding⟩
  intro h
  have : p = p ∘ e ∘ e.symm.toEmbedding := by
    ext
    simp
  rw [this]
  exact h.comp_embedding e.symm.toEmbedding
Affine Independence is Preserved Under Index Equivalence
Informal description
Let $k$ be a field and $P$ be an affine space over $k$. Given an equivalence (bijection) $e : \iota \simeq \iota'$ between index types $\iota$ and $\iota'$, and a family of points $p : \iota' \to P$, the following are equivalent: 1. The family $p \circ e : \iota \to P$ is affinely independent. 2. The family $p : \iota' \to P$ is affinely independent.
AffineIndependent.mono theorem
{s t : Set P} (ha : AffineIndependent k (fun x => x : t → P)) (hs : s ⊆ t) : AffineIndependent k (fun x => x : s → P)
Full source 
/-- If a set of points is affinely independent, so is any subset. -/
protected theorem AffineIndependent.mono {s t : Set P}
    (ha : AffineIndependent k (fun x => x : t → P)) (hs : s ⊆ t) :
    AffineIndependent k (fun x => x : s → P) :=
  ha.comp_embedding (s.embeddingOfSubset t hs)
Affine Independence is Preserved Under Subset Inclusion
Informal description
Let $P$ be an affine space over a field $k$, and let $s, t \subseteq P$ be subsets such that $s \subseteq t$. If the inclusion map $t \to P$ is affinely independent, then the inclusion map $s \to P$ is also affinely independent.
AffineIndependent.of_set_of_injective theorem
{p : ι → P} (ha : AffineIndependent k (fun x => x : Set.range p → P)) (hi : Function.Injective p) : AffineIndependent k p
Full source 
/-- If the range of an injective indexed family of points is affinely
independent, so is that family. -/
theorem AffineIndependent.of_set_of_injective {p : ι → P}
    (ha : AffineIndependent k (fun x => x : Set.range p → P)) (hi : Function.Injective p) :
    AffineIndependent k p :=
  ha.comp_embedding
    (⟨fun i => ⟨p i, Set.mem_range_self _⟩, fun _ _ h => hi (Subtype.mk_eq_mk.1 h)⟩ :
      ι ↪ Set.range p)
Affine Independence via Range Restriction and Injectivity
Informal description
Let $k$ be a field and $P$ an affine space over $k$. Given an indexed family of points $p : \iota \to P$, if: 1. The family obtained by restricting to the range of $p$ (i.e., $\lambda x, x : \mathrm{range}\, p \to P$) is affinely independent, and 2. The indexing function $p$ is injective, then the original family $p$ is affinely independent.
AffineIndependent.of_comp theorem
{p : ι → P} (f : P →ᵃ[k] P₂) (hai : AffineIndependent k (f ∘ p)) : AffineIndependent k p
Full source 
/-- 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.of_comp {p : ι → P} (f : P →ᵃ[k] P₂) (hai : AffineIndependent k (f ∘ p)) :
    AffineIndependent k p := by
  rcases isEmpty_or_nonempty ι with h | h
  · haveI := h
    apply affineIndependent_of_subsingleton
  obtain ⟨i⟩ := h
  rw [affineIndependent_iff_linearIndependent_vsub k p i]
  simp_rw [affineIndependent_iff_linearIndependent_vsub k (f ∘ p) i, Function.comp_apply, ←
    f.linearMap_vsub] at hai
  exact LinearIndependent.of_comp f.linear hai
Affine Independence of Original Family via Affine Independence of Image under Affine Map
Informal description
Let $k$ be a ring, $P$ and $P_2$ be affine spaces over $k$ with associated vector spaces $V$ and $V_2$ respectively, and $p : \iota \to P$ be a family of points in $P$. Given an affine map $f : P \to P_2$, if the image family $f \circ p : \iota \to P_2$ is affinely independent, then the original family $p$ is also affinely independent.
AffineIndependent.map' theorem
{p : ι → P} (hai : AffineIndependent k p) (f : P →ᵃ[k] P₂) (hf : Function.Injective f) : AffineIndependent k (f ∘ p)
Full source 
/-- The image of a family of points in affine space, under an injective affine transformation, is
affine-independent. -/
theorem AffineIndependent.map' {p : ι → P} (hai : AffineIndependent k p) (f : P →ᵃ[k] P₂)
    (hf : Function.Injective f) : AffineIndependent k (f ∘ p) := by
  rcases isEmpty_or_nonempty ι with h | h
  · haveI := h
    apply affineIndependent_of_subsingleton
  obtain ⟨i⟩ := h
  rw [affineIndependent_iff_linearIndependent_vsub k p i] at hai
  simp_rw [affineIndependent_iff_linearIndependent_vsub k (f ∘ p) i, Function.comp_apply, ←
    f.linearMap_vsub]
  have hf' : LinearMap.ker f.linear = ⊥ := by rwa [LinearMap.ker_eq_bot, f.linear_injective_iff]
  exact LinearIndependent.map' hai f.linear hf'
Preservation of affine independence under injective affine maps
Informal description
Let $k$ be a ring, $P$ and $P_2$ be affine spaces over $k$ with associated vector spaces $V$ and $V_2$ respectively. Given an affinely independent family of points $p : \iota \to P$ and an injective affine map $f : P \to P_2$, the image family $f \circ p : \iota \to P_2$ is also affinely independent.
AffineMap.affineIndependent_iff theorem
{p : ι → P} (f : P →ᵃ[k] P₂) (hf : Function.Injective f) : AffineIndependent k (f ∘ p) ↔ AffineIndependent k p
Full source 
/-- Injective affine maps preserve affine independence. -/
theorem AffineMap.affineIndependent_iff {p : ι → P} (f : P →ᵃ[k] P₂) (hf : Function.Injective f) :
    AffineIndependentAffineIndependent k (f ∘ p) ↔ AffineIndependent k p :=
  ⟨AffineIndependent.of_comp f, fun hai => AffineIndependent.map' hai f hf⟩
Affine Independence Preservation under Injective Affine Maps: $f \circ p$ affinely independent $\leftrightarrow$ $p$ affinely independent
Informal description
Let $k$ be a ring, $P$ and $P_2$ be affine spaces over $k$ with associated vector spaces $V$ and $V_2$ respectively, and $p : \iota \to P$ be a family of points in $P$. Given an injective affine map $f : P \to P_2$, the image family $f \circ p : \iota \to P_2$ is affinely independent if and only if the original family $p$ is affinely independent.
AffineEquiv.affineIndependent_iff theorem
{p : ι → P} (e : P ≃ᵃ[k] P₂) : AffineIndependent k (e ∘ p) ↔ AffineIndependent k p
Full source 
/-- Affine equivalences preserve affine independence of families of points. -/
theorem AffineEquiv.affineIndependent_iff {p : ι → P} (e : P ≃ᵃ[k] P₂) :
    AffineIndependentAffineIndependent k (e ∘ p) ↔ AffineIndependent k p :=
  e.toAffineMap.affineIndependent_iff e.toEquiv.injective
Affine Independence Preservation under Affine Equivalence: $e \circ p$ affinely independent $\leftrightarrow$ $p$ affinely independent
Informal description
Let $k$ be a ring, $P$ and $P_2$ be affine spaces over $k$, and $e : P \simeqᵃ[k] P_2$ be an affine equivalence. For any family of points $p : \iota \to P$, the image family $e \circ p : \iota \to P_2$ is affinely independent if and only if the original family $p$ is affinely independent.
AffineEquiv.affineIndependent_set_of_eq_iff theorem
{s : Set P} (e : P ≃ᵃ[k] P₂) : AffineIndependent k ((↑) : e '' s → P₂) ↔ AffineIndependent k ((↑) : s → P)
Full source 
/-- Affine equivalences preserve affine independence of subsets. -/
theorem AffineEquiv.affineIndependent_set_of_eq_iff {s : Set P} (e : P ≃ᵃ[k] P₂) :
    AffineIndependentAffineIndependent k ((↑) : e '' s → P₂) ↔ AffineIndependent k ((↑) : s → P) := by
  have : e ∘ ((↑) : s → P) = ((↑) : e '' s → P₂) ∘ (e : P ≃ P₂).image s := rfl
  -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
  erw [← e.affineIndependent_iff, this, affineIndependent_equiv]
Affine Independence Preservation under Affine Equivalence for Subsets
Informal description
Let $k$ be a ring, $P$ and $P_2$ be affine spaces over $k$, and $e : P \simeqᵃ[k] P_2$ be an affine equivalence. For any subset $s \subseteq P$, the family of points in the image $e(s) \subseteq P_2$ is affinely independent if and only if the family of points in $s$ is affinely independent.
AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan theorem
[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
Full source 
/-- 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.exists_mem_inter_of_exists_mem_inter_affineSpan [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 := by
  rw [Set.image_eq_range] at hp0s1 hp0s2
  rw [mem_affineSpan_iff_eq_affineCombination, ←
    Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype] at hp0s1 hp0s2
  rcases hp0s1 with ⟨fs1, hfs1, w1, hw1, hp0s1⟩
  rcases hp0s2 with ⟨fs2, hfs2, w2, hw2, hp0s2⟩
  rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq] at ha
  replace ha := ha fs1 fs2 w1 w2 hw1 hw2 (hp0s1 ▸ hp0s2)
  have hnz : ∑ i ∈ fs1, w1 i∑ i ∈ fs1, w1 i ≠ 0 := hw1.symm ▸ one_ne_zero
  rcases Finset.exists_ne_zero_of_sum_ne_zero hnz with ⟨i, hifs1, hinz⟩
  simp_rw [← Set.indicator_of_mem (Finset.mem_coe.2 hifs1) w1, ha] at hinz
  use i, hfs1 hifs1
  exact hfs2 (Set.mem_of_indicator_ne_zero hinz)
Common Index in Affine Spans of Affinely Independent Family
Informal description
Let $k$ be a nontrivial ring and $P$ an affine space over $k$. Given an affinely independent family of points $p \colon \iota \to P$ and two subsets $s_1, s_2 \subseteq \iota$, if a point $p_0 \in P$ lies in both the affine span of $p(s_1)$ and the affine span of $p(s_2)$, then there exists an index $i \in \iota$ such that $i \in s_1 \cap s_2$.
AffineIndependent.affineSpan_disjoint_of_disjoint theorem
[Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) {s1 s2 : Set ι} (hd : Disjoint s1 s2) : Disjoint (affineSpan k (p '' s1) : Set P) (affineSpan k (p '' s2))
Full source 
/-- 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. -/
theorem AffineIndependent.affineSpan_disjoint_of_disjoint [Nontrivial k] {p : ι → P}
    (ha : AffineIndependent k p) {s1 s2 : Set ι} (hd : Disjoint s1 s2) :
    Disjoint (affineSpan k (p '' s1) : Set P) (affineSpan k (p '' s2)) := by
  refine Set.disjoint_left.2 fun p0 hp0s1 hp0s2 => ?_
  obtain ⟨i, hi⟩ := ha.exists_mem_inter_of_exists_mem_inter_affineSpan hp0s1 hp0s2
  exact Set.disjoint_iff.1 hd hi
Disjointness of Affine Spans for Affinely Independent Families
Informal description
Let $k$ be a nontrivial ring and $P$ an affine space over $k$. Given an affinely independent family of points $p \colon \iota \to P$ and two disjoint subsets $s_1, s_2 \subseteq \iota$, the affine spans of $p(s_1)$ and $p(s_2)$ are disjoint as subsets of $P$.
AffineIndependent.mem_affineSpan_iff theorem
[Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) (i : ι) (s : Set ι) : p i ∈ affineSpan k (p '' s) ↔ i ∈ s
Full source 
/-- 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. -/
@[simp]
protected theorem AffineIndependent.mem_affineSpan_iff [Nontrivial k] {p : ι → P}
    (ha : AffineIndependent k p) (i : ι) (s : Set ι) : p i ∈ affineSpan k (p '' s)p i ∈ affineSpan k (p '' s) ↔ i ∈ s := by
  constructor
  · intro hs
    have h :=
      AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan ha hs
        (mem_affineSpan k (Set.mem_image_of_mem _ (Set.mem_singleton _)))
    rwa [← Set.nonempty_def, Set.inter_singleton_nonempty] at h
  · exact fun h => mem_affineSpan k (Set.mem_image_of_mem p h)
Characterization of Affine Span Membership for Affinely Independent Points
Informal description
Let $k$ be a nontrivial ring and $P$ an affine space over $k$. Given an affinely independent family of points $\{p_i\}_{i \in \iota}$ in $P$, for any index $i \in \iota$ and subset $s \subseteq \iota$, the point $p_i$ belongs to the affine span of $\{p_j \mid j \in s\}$ if and only if $i \in s$.
AffineIndependent.not_mem_affineSpan_diff theorem
[Nontrivial k] {p : ι → P} (ha : AffineIndependent k p) (i : ι) (s : Set ι) : p i ∉ affineSpan k (p '' (s \ { i }))
Full source 
/-- 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.not_mem_affineSpan_diff [Nontrivial k] {p : ι → P}
    (ha : AffineIndependent k p) (i : ι) (s : Set ι) : p i ∉ affineSpan k (p '' (s \ {i})) := by
  simp [ha]
Affinely independent points lie outside affine span of others
Informal description
Let $k$ be a nontrivial ring, $P$ an affine space over a module $V$ with scalar ring $k$, and $\{p_i\}_{i \in \iota}$ a family of points in $P$. If the family is affinely independent, then for any index $i \in \iota$ and any subset $s \subseteq \iota$, the point $p_i$ does not belong to the affine span of the remaining points $\{p_j \mid j \in s \setminus \{i\}\}$.
exists_nontrivial_relation_sum_zero_of_not_affine_ind theorem
{t : Finset V} (h : ¬AffineIndependent k ((↑) : t → V)) : ∃ f : V → k, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0
Full source 
theorem exists_nontrivial_relation_sum_zero_of_not_affine_ind {t : Finset V}
    (h : ¬AffineIndependent k ((↑) : t → V)) :
    ∃ f : V → k, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0 := by
  classical
    rw [affineIndependent_iff_of_fintype] at h
    simp only [exists_prop, not_forall] at h
    obtain ⟨w, hw, hwt, i, hi⟩ := h
    simp only [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w ((↑) : t → V) hw 0,
      vsub_eq_sub, Finset.weightedVSubOfPoint_apply, sub_zero] at hwt
    let f : ∀ x : V, x ∈ t → k := fun x hx => w ⟨x, hx⟩
    refine ⟨fun x => if hx : x ∈ t then f x hx else (0 : k), ?_, ?_, by use i; simp [f, hi]⟩
    on_goal 1 =>
      suffices (∑ e ∈ t, dite (e ∈ t) (fun hx => f e hx • e) fun _ => 0) = 0 by
        convert this
        rename V => x
        by_cases hx : x ∈ t <;> simp [hx]
    all_goals
      simp only [f, Finset.sum_dite_of_true fun _ h => h, Finset.mk_coe, hwt, hw]
Existence of Nontrivial Linear Relation for Non-Affinely-Independent Points
Informal description
Let $V$ be a vector space over a field $k$, and let $t$ be a finite subset of $V$. If the inclusion map $(\cdot) : t \to V$ is not affinely independent, then there exists a function $f : V \to k$ such that: 1. $\sum_{e \in t} f(e) \cdot e = 0$, 2. $\sum_{e \in t} f(e) = 0$, and 3. There exists some $x \in t$ with $f(x) \neq 0$.
affineIndependent_iff theorem
{ι} {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
Full source 
/-- Viewing a module as an affine space modelled on itself, we can characterise affine independence
in terms of linear combinations. -/
theorem affineIndependent_iff {ι} {p : ι → V} :
    AffineIndependentAffineIndependent k p ↔
      ∀ (s : Finset ι) (w : ι → k), s.sum w = 0 → ∑ e ∈ s, w e • p e = 0 → ∀ e ∈ s, w e = 0 :=
  forall₃_congr fun s w hw => by simp [s.weightedVSub_eq_linear_combination hw]
Characterization of Affine Independence via Linear Combinations
Informal description
A family of points $\{p_i\}_{i \in \iota}$ in a vector space $V$ over a field $k$ is affinely independent if and only if for every finite subset $s \subset \iota$ and every set of weights $\{w_i\}_{i \in \iota}$ in $k$ with $\sum_{i \in s} w_i = 0$, the condition $\sum_{i \in s} w_i p_i = 0$ implies that $w_i = 0$ for all $i \in s$.
weightedVSub_mem_vectorSpan_pair theorem
{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 ({s.affineCombination k p w₁, s.affineCombination k p w₂} : Set P) ↔ ∃ r : k, ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
Full source 
/-- 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 weightedVSub_mem_vectorSpan_pair {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 ({s.affineCombination k p w₁, s.affineCombination k p w₂} : Set P)s.weightedVSub p w ∈
        vectorSpan k ({s.affineCombination k p w₁, s.affineCombination k p w₂} : Set P) ↔
      ∃ r : k, ∀ i ∈ s, w i = r * (w₁ i - w₂ i) := by
  rw [mem_vectorSpan_pair]
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rcases h with ⟨r, hr⟩
    refine ⟨r, fun i hi => ?_⟩
    rw [s.affineCombination_vsub, ← s.weightedVSub_const_smul, ← sub_eq_zero, ← map_sub] at hr
    have hw' : (∑ j ∈ s, (r • (w₁ - w₂) - w) j) = 0 := by
      simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
    have hr' := h s _ hw' hr i hi
    rw [eq_comm, ← sub_eq_zero, ← smul_eq_mul]
    exact hr'
  · rcases h with ⟨r, hr⟩
    refine ⟨r, ?_⟩
    let w' i := r * (w₁ i - w₂ i)
    change ∀ i ∈ s, w i = w' i at hr
    rw [s.weightedVSub_congr hr fun _ _ => rfl, s.affineCombination_vsub, ←
      s.weightedVSub_const_smul]
    congr
Weighted subtraction in vector span of two affine combinations
Informal description
Let $p \colon \iota \to P$ be an affinely independent family of points in an affine space over a ring $k$. Let $w, w_1, w_2 \colon \iota \to k$ be weight functions and $s$ a finite subset of $\iota$ such that: 1. $\sum_{i \in s} w_i = 0$ (weights sum to zero) 2. $\sum_{i \in s} w_{1,i} = 1$ ($w_1$ is an affine combination) 3. $\sum_{i \in s} w_{2,i} = 1$ ($w_2$ is an affine combination) Then the weighted subtraction $\sum_{i \in s} w_i (p_i - p_j)$ (for some fixed $j \in s$) lies in the vector span of the two affine combinations $\sum_{i \in s} w_{1,i} p_i$ and $\sum_{i \in s} w_{2,i} p_i$ if and only if there exists a scalar $r \in k$ such that for all $i \in s$, $w_i = r (w_{1,i} - w_{2,i})$.
affineCombination_mem_affineSpan_pair theorem
{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) : s.affineCombination k p w ∈ line[k, s.affineCombination k p w₁, s.affineCombination k p w₂] ↔ ∃ r : k, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
Full source 
/-- 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 affineCombination_mem_affineSpan_pair {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) :
    s.affineCombination k p w ∈ line[k, s.affineCombination k p w₁, s.affineCombination k p w₂]s.affineCombination k p w ∈ line[k, s.affineCombination k p w₁, s.affineCombination k p w₂] ↔
      ∃ r : k, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i := by
  rw [← vsub_vadd (s.affineCombination k p w) (s.affineCombination k p w₁),
    AffineSubspace.vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _),
    direction_affineSpan, s.affineCombination_vsub, Set.pair_comm,
    weightedVSub_mem_vectorSpan_pair h _ hw₂ hw₁]
  · simp only [Pi.sub_apply, sub_eq_iff_eq_add]
  · simp_all only [Pi.sub_apply, Finset.sum_sub_distrib, sub_self]
Affine Combination in Span of Two Points if and only if Weights are Affine Combination of Differences
Informal description
Let $p \colon \iota \to P$ be an affinely independent family of points in an affine space over a ring $k$. Let $w, w_1, w_2 \colon \iota \to k$ be weight functions and $s$ a finite subset of $\iota$ such that: 1. $\sum_{i \in s} w_i = 1$ ($w$ is an affine combination) 2. $\sum_{i \in s} w_{1,i} = 1$ ($w_1$ is an affine combination) 3. $\sum_{i \in s} w_{2,i} = 1$ ($w_2$ is an affine combination) Then the affine combination $\sum_{i \in s} w_i p_i$ lies in the affine span of the two points $\sum_{i \in s} w_{1,i} p_i$ and $\sum_{i \in s} w_{2,i} p_i$ if and only if there exists a scalar $r \in k$ such that for all $i \in s$, $w_i = r (w_{2,i} - w_{1,i}) + w_{1,i}$.
exists_subset_affineIndependent_affineSpan_eq_top theorem
{s : Set P} (h : AffineIndependent k (fun p => p : s → P)) : ∃ t : Set P, s ⊆ t ∧ AffineIndependent k (fun p => p : t → P) ∧ affineSpan k t = ⊤
Full source 
/-- An affinely independent set of points can be extended to such a
set that spans the whole space. -/
theorem exists_subset_affineIndependent_affineSpan_eq_top {s : Set P}
    (h : AffineIndependent k (fun p => p : s → P)) :
    ∃ t : Set P, s ⊆ t ∧ AffineIndependent k (fun p => p : t → P) ∧ affineSpan k t = ⊤ := by
  rcases s.eq_empty_or_nonempty with (rfl | ⟨p₁, hp₁⟩)
  · have p₁ : P := AddTorsor.nonempty.some
    let hsv := Basis.ofVectorSpace k V
    have hsvi := hsv.linearIndependent
    have hsvt := hsv.span_eq
    rw [Basis.coe_ofVectorSpace] at hsvi hsvt
    have h0 : ∀ v : V, v ∈ Basis.ofVectorSpaceIndex k V → v ≠ 0 := by
      intro v hv
      simpa [hsv] using hsv.ne_zero ⟨v, hv⟩
    rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k h0 p₁] at hsvi
    exact
      ⟨{p₁} ∪ (fun v => v +ᵥ p₁) '' _, Set.empty_subset _, hsvi,
        affineSpan_singleton_union_vadd_eq_top_of_span_eq_top p₁ hsvt⟩
  · rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁] at h
    let bsv := Basis.extend h
    have hsvi := bsv.linearIndependent
    have hsvt := bsv.span_eq
    rw [Basis.coe_extend] at hsvi hsvt
    rw [linearIndependent_subtype_iff] at hsvi h
    have hsv := h.subset_extend (Set.subset_univ _)
    have h0 : ∀ v : V, v ∈ h.extend (Set.subset_univ _) → v ≠ 0 := by
      intro v hv
      simpa [bsv] using bsv.ne_zero ⟨v, hv⟩
    rw [← linearIndependent_subtype_iff,
      linearIndependent_set_iff_affineIndependent_vadd_union_singleton k h0 p₁] at hsvi
    refine ⟨{p₁} ∪ (fun v => v +ᵥ p₁) '' h.extend (Set.subset_univ _), ?_, ?_⟩
    · refine Set.Subset.trans ?_ (Set.union_subset_union_right _ (Set.image_subset _ hsv))
      simp [Set.image_image]
    · use hsvi
      exact affineSpan_singleton_union_vadd_eq_top_of_span_eq_top p₁ hsvt
Extension of Affinely Independent Set to a Spanning Set
Informal description
Let $P$ be an affine space over a field $k$, and let $s \subseteq P$ be an affinely independent set of points. Then there exists a set $t \subseteq P$ containing $s$ that is affinely independent and whose affine span is the entire space $P$.
exists_affineIndependent theorem
(s : Set P) : ∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k ((↑) : t → P)
Full source 
theorem exists_affineIndependent (s : Set P) :
    ∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k ((↑) : t → P) := by
  rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)
  · exact ⟨∅, Set.empty_subset ∅, rfl, affineIndependent_of_subsingleton k _⟩
  obtain ⟨b, hb₁, hb₂, hb₃⟩ := exists_linearIndependent k ((Equiv.vaddConst p).symm '' s)
  have hb₀ : ∀ v : V, v ∈ b → v ≠ 0 := fun v hv => hb₃.ne_zero (⟨v, hv⟩ : b)
  rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k hb₀ p] at hb₃
  refine ⟨{p} ∪ Equiv.vaddConst p '' b, ?_, ?_, hb₃⟩
  · apply Set.union_subset (Set.singleton_subset_iff.mpr hp)
    rwa [← (Equiv.vaddConst p).subset_symm_image b s]
  · rw [Equiv.coe_vaddConst_symm, ← vectorSpan_eq_span_vsub_set_right k hp] at hb₂
    apply AffineSubspace.ext_of_direction_eq
    · have : Submodule.span k b = Submodule.span k (insert 0 b) := by simp
      simp only [direction_affineSpan, ← hb₂, Equiv.coe_vaddConst, Set.singleton_union,
        vectorSpan_eq_span_vsub_set_right k (Set.mem_insert p _), this]
      congr
      change (Equiv.vaddConst p).symm '' insert p (Equiv.vaddConst p '' b) = _
      rw [Set.image_insert_eq, ← Set.image_comp]
      simp
    · use p
      simp only [Equiv.coe_vaddConst, Set.singleton_union, Set.mem_inter_iff]
      exact ⟨mem_affineSpan k (Set.mem_insert p _), mem_affineSpan k hp⟩
Existence of Affinely Independent Spanning Subset in Affine Spaces
Informal description
For any set $s$ of points in an affine space $P$ over a field $k$, there exists a subset $t \subseteq s$ such that: 1. The affine span of $t$ equals the affine span of $s$, and 2. The family of points in $t$ is affinely independent.
affineIndependent_of_ne theorem
{p₁ p₂ : P} (h : p₁ ≠ p₂) : AffineIndependent k ![p₁, p₂]
Full source 
/-- Two different points are affinely independent. -/
theorem affineIndependent_of_ne {p₁ p₂ : P} (h : p₁ ≠ p₂) : AffineIndependent k ![p₁, p₂] := by
  rw [affineIndependent_iff_linearIndependent_vsub k ![p₁, p₂] 0]
  let i₁ : { x // x ≠ (0 : Fin 2) } := ⟨1, by norm_num⟩
  have he' : ∀ i, i = i₁ := by
    rintro ⟨i, hi⟩
    ext
    fin_cases i
    · simp at hi
    · simp [i₁]
  haveI : Unique { x // x ≠ (0 : Fin 2) } := ⟨⟨i₁⟩, he'⟩
  apply linearIndependent_unique
  rw [he' default]
  simpa using h.symm
Affine Independence of Two Distinct Points
Informal description
For any two distinct points $p_1$ and $p_2$ in an affine space over a field $k$, the family of points $(p_1, p_2)$ is affinely independent.
AffineIndependent.affineIndependent_of_not_mem_span theorem
{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
Full source 
/-- 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.affineIndependent_of_not_mem_span {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 := by
  classical
    intro s w hw hs
    let s' : Finset { y // y ≠ i } := s.subtype (· ≠ i)
    let p' : { y // y ≠ i } → P := fun x => p x
    by_cases his : i ∈ s ∧ w i ≠ 0
    · refine False.elim (hi ?_)
      let wm : ι → k := -(w i)⁻¹ • w
      have hms : s.weightedVSub p wm = (0 : V) := by simp [wm, hs]
      have hwm : ∑ i ∈ s, wm i = 0 := by simp [wm, ← Finset.mul_sum, hw]
      have hwmi : wm i = -1 := by simp [wm, his.2]
      let w' : { y // y ≠ i } → k := fun x => wm x
      have hw' : ∑ x ∈ s', w' x = 1 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [← s.sum_filter_add_sum_filter_not (· ≠ i)] at hwm
        simpa only [not_not, Finset.filter_eq' _ i, if_pos his.1, sum_singleton, hwmi,
          add_neg_eq_zero] using hwm
      rw [← s.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one hms his.1 hwmi, ←
        (Subtype.range_coe : _ = { x | x ≠ i }), ← Set.range_comp, ←
        s.affineCombination_subtype_eq_filter]
      exact affineCombination_mem_affineSpan hw' p'
    · rw [not_and_or, Classical.not_not] at his
      let w' : { y // y ≠ i } → k := fun x => w x
      have hw' : ∑ x ∈ s', w' x = 0 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [Finset.sum_filter_of_ne, hw]
        rintro x hxs hwx rfl
        exact hwx (his.neg_resolve_left hxs)
      have hs' : s'.weightedVSub p' w' = (0 : V) := by
        simp_rw [w', s', p', Finset.weightedVSub_subtype_eq_filter]
        rw [Finset.weightedVSub_filter_of_ne, hs]
        rintro x hxs hwx rfl
        exact hwx (his.neg_resolve_left hxs)
      intro j hj
      by_cases hji : j = i
      · rw [hji] at hj
        exact hji.symm ▸ his.neg_resolve_left hj
      · exact ha s' w' hw' hs' ⟨j, hji⟩ (Finset.mem_subtype.2 hj)
Affine Independence via Exclusion of a Point Outside the Span
Informal description
Let $p : \iota \to P$ be a family of points in an affine space over a field $k$, and let $i \in \iota$. Suppose that the subfamily obtained by excluding $p_i$ is affinely independent, and that $p_i$ does not lie in the affine span of the remaining points $\{p_j \mid j \neq i\}$. Then the entire family $p$ is affinely independent.
affineIndependent_of_ne_of_mem_of_mem_of_not_mem theorem
{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₃]
Full source 
/-- 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_mem_of_not_mem {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₃] := by
  have ha : AffineIndependent k fun x : { x : Fin 3 // x ≠ 2 } => ![p₁, p₂, p₃] x := by
    rw [← affineIndependent_equiv (finSuccAboveEquiv (2 : Fin 3))]
    convert affineIndependent_of_ne k hp₁p₂
    ext x
    fin_cases x <;> rfl
  refine ha.affineIndependent_of_not_mem_span ?_
  intro h
  refine hp₃ ((AffineSubspace.le_def' _ s).1 ?_ p₃ h)
  simp_rw [affineSpan_le, Set.image_subset_iff, Set.subset_def, Set.mem_preimage]
  intro x
  fin_cases x <;> simp +decide [hp₁, hp₂]
Affine Independence of Three Points with Two in a Subspace and One Outside
Informal description
Let $k$ be a field, $P$ an affine space over $k$, and $s$ an affine subspace of $P$. For any three distinct points $p_1, p_2, p_3 \in P$ such that: 1. $p_1 \neq p_2$, 2. $p_1, p_2 \in s$, 3. $p_3 \notin s$, the family of points $(p_1, p_2, p_3)$ is affinely independent.
affineIndependent_of_ne_of_mem_of_not_mem_of_mem theorem
{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₃]
Full source 
/-- 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_not_mem_of_mem {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₃] := by
  rw [← affineIndependent_equiv (Equiv.swap (1 : Fin 3) 2)]
  convert affineIndependent_of_ne_of_mem_of_mem_of_not_mem hp₁p₃ hp₁ hp₃ hp₂ using 1
  ext x
  fin_cases x <;> rfl
Affine Independence of Three Points with Two in a Subspace and One Outside (Variant)
Informal description
Let $k$ be a field, $P$ an affine space over $k$, and $s$ an affine subspace of $P$. For any three distinct points $p_1, p_2, p_3 \in P$ such that: 1. $p_1 \neq p_3$, 2. $p_1, p_3 \in s$, 3. $p_2 \notin s$, the family of points $(p_1, p_2, p_3)$ is affinely independent.
affineIndependent_of_ne_of_not_mem_of_mem_of_mem theorem
{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₃]
Full source 
/-- If distinct points `p₂` and `p₃` lie in `s` but `p₁` does not, the three points are affinely
independent. -/
theorem affineIndependent_of_ne_of_not_mem_of_mem_of_mem {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₃] := by
  rw [← affineIndependent_equiv (Equiv.swap (0 : Fin 3) 2)]
  convert affineIndependent_of_ne_of_mem_of_mem_of_not_mem hp₂p₃.symm hp₃ hp₂ hp₁ using 1
  ext x
  fin_cases x <;> rfl
Affine Independence of Three Points with One Outside and Two in a Subspace
Informal description
Let $k$ be a field, $P$ an affine space over $k$, and $s$ an affine subspace of $P$. For any three distinct points $p_1, p_2, p_3 \in P$ such that: 1. $p_2 \neq p_3$, 2. $p_1 \notin s$, 3. $p_2, p_3 \in s$, the family of points $(p_1, p_2, p_3)$ is affinely independent.
sign_eq_of_affineCombination_mem_affineSpan_pair theorem
{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 : s.affineCombination k p w ∈ line[k, s.affineCombination k p w₁, s.affineCombination k 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)
Full source 
/-- 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. -/
theorem sign_eq_of_affineCombination_mem_affineSpan_pair {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 :
      s.affineCombination k p w ∈ line[k, s.affineCombination k p w₁, s.affineCombination k 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) := by
  rw [affineCombination_mem_affineSpan_pair h hw hw₁ hw₂] at hs
  rcases hs with ⟨r, hr⟩
  rw [hr i hi, hr j hj, hi0, hj0, add_zero, add_zero, sub_zero, sub_zero, sign_mul, sign_mul, hij]
Sign Consistency of Weights in Affine Span Condition
Informal description
Let $p \colon \iota \to P$ be an affinely independent family of points in an affine space over a ring $k$. Let $w, w_1, w_2 \colon \iota \to k$ be weight functions and $s$ a finite subset of $\iota$ such that: 1. $\sum_{i \in s} w_i = 1$ (affine combination condition for $w$) 2. $\sum_{i \in s} w_{1,i} = 1$ (affine combination condition for $w_1$) 3. $\sum_{i \in s} w_{2,i} = 1$ (affine combination condition for $w_2$) Suppose that the affine combination $\sum_{i \in s} w_i p_i$ lies in the affine span of the two points $\sum_{i \in s} w_{1,i} p_i$ and $\sum_{i \in s} w_{2,i} p_i$. If for two indices $i, j \in s$: 1. $w_{1,i} = 0$ and $w_{1,j} = 0$ 2. $\text{sign}(w_{2,i}) = \text{sign}(w_{2,j})$ then $\text{sign}(w_i) = \text{sign}(w_j)$.
sign_eq_of_affineCombination_mem_affineSpan_single_lineMap theorem
{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 : s.affineCombination k p w ∈ line[k, p i₁, AffineMap.lineMap (p i₂) (p i₃) c]) : SignType.sign (w i₂) = SignType.sign (w i₃)
Full source 
/-- 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. -/
theorem sign_eq_of_affineCombination_mem_affineSpan_single_lineMap {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 : s.affineCombination k p w ∈ line[k, p i₁, AffineMap.lineMap (p i₂) (p i₃) c]) :
    SignType.sign (w i₂) = SignType.sign (w i₃) := by
  classical
    rw [← s.affineCombination_affineCombinationSingleWeights k p h₁, ←
      s.affineCombination_affineCombinationLineMapWeights p h₂ h₃ c] at hs
    refine
      sign_eq_of_affineCombination_mem_affineSpan_pair h hw
        (s.sum_affineCombinationSingleWeights k h₁)
        (s.sum_affineCombinationLineMapWeights h₂ h₃ c) hs h₂ h₃
        (Finset.affineCombinationSingleWeights_apply_of_ne k h₁₂.symm)
        (Finset.affineCombinationSingleWeights_apply_of_ne k h₁₃.symm) ?_
    rw [Finset.affineCombinationLineMapWeights_apply_left h₂₃,
      Finset.affineCombinationLineMapWeights_apply_right h₂₃]
    simp_all only [sub_pos, sign_pos]
Sign Consistency of Weights in Affine Span Condition for Linearly Interpolated Points
Informal description
Let $p \colon \iota \to P$ be an affinely independent family of points in an affine space over a ring $k$. Let $w \colon \iota \to k$ be a weight function and $s$ a finite subset of $\iota$ such that $\sum_{i \in s} w_i = 1$ (affine combination condition). For three distinct indices $i_1, i_2, i_3 \in s$ with $i_1 \neq i_2$, $i_1 \neq i_3$, and $i_2 \neq i_3$, and a parameter $c \in k$ with $0 < c < 1$, suppose that the affine combination $\sum_{i \in s} w_i p_i$ lies in the affine span of the point $p_{i_1}$ and the point obtained by the line map $c \cdot (p_{i_3} - p_{i_2}) + p_{i_2}$ between $p_{i_2}$ and $p_{i_3}$. Then the signs of the weights $w_{i_2}$ and $w_{i_3}$ are equal, i.e., $\text{sign}(w_{i_2}) = \text{sign}(w_{i_3})$.
Affine.Simplex structure
(n : ℕ)
Full source 
/-- A `Simplex k P n` is a collection of `n + 1` affinely
independent points. -/
structure Simplex (n : ℕ) where
  points : Fin (n + 1) → P
  independent : AffineIndependent k points
Simplex in Affine Space
Informal description
A `Simplex k P n` is a structure representing a collection of `n + 1` affinely independent points in an affine space over a field `k`. Here, `P` denotes the type of points in the affine space, and `n` is the dimension of the simplex. Affine independence means that no nontrivial weighted subtraction of these points results in the zero vector, which is equivalent to the linear independence of the vectors obtained by subtracting a base point from the other points in the family.
Affine.Triangle abbrev
Full source 
/-- A `Triangle k P` is a collection of three affinely independent points. -/
abbrev Triangle :=
  Simplex k P 2
Affine Triangle of Three Independent Points
Informal description
A `Triangle k P` is a collection of three affinely independent points in an affine space over a field `k`, where `P` denotes the type of points in the affine space.
Affine.Simplex.mkOfPoint definition
(p : P) : Simplex k P 0
Full source 
/-- Construct a 0-simplex from a point. -/
def mkOfPoint (p : P) : Simplex k P 0 :=
  have : Subsingleton (Fin (1 + 0)) := by rw [add_zero]; infer_instance
  ⟨fun _ => p, affineIndependent_of_subsingleton k _⟩
0-simplex from a point
Informal description
Given a point \( p \) in an affine space \( P \) over a field \( k \), the function constructs a 0-dimensional simplex (a single point) where all points in the simplex are equal to \( p \). This is well-defined because the index set for a 0-dimensional simplex is a subsingleton (has at most one element).
Affine.Simplex.mkOfPoint_points theorem
(p : P) (i : Fin 1) : (mkOfPoint k p).points i = p
Full source 
/-- The point in a simplex constructed with `mkOfPoint`. -/
@[simp]
theorem mkOfPoint_points (p : P) (i : Fin 1) : (mkOfPoint k p).points i = p :=
  rfl
Points in a 0-Simplex Constructed from a Single Point
Informal description
For any point $p$ in an affine space $P$ over a field $k$ and any index $i$ in the finite set $\text{Fin}\,1$, the $i$-th point of the $0$-simplex constructed from $p$ is equal to $p$, i.e., $(\text{mkOfPoint}\,k\,p).\text{points}\,i = p$.
Affine.Simplex.instInhabitedOfNatNat instance
[Inhabited P] : Inhabited (Simplex k P 0)
Full source 
instance [Inhabited P] : Inhabited (Simplex k P 0) :=
  ⟨mkOfPoint k default⟩
Inhabitedness of 0-Simplices in Affine Spaces
Informal description
For any affine space $P$ over a field $k$ with an inhabited type structure, the type of $0$-dimensional simplices in $P$ is also inhabited.
Affine.Simplex.ext theorem
{n : ℕ} {s1 s2 : Simplex k P n} (h : ∀ i, s1.points i = s2.points i) : s1 = s2
Full source 
/-- Two simplices are equal if they have the same points. -/
@[ext]
theorem ext {n : ℕ} {s1 s2 : Simplex k P n} (h : ∀ i, s1.points i = s2.points i) : s1 = s2 := by
  cases s1
  cases s2
  congr with i
  exact h i
Equality of Simplices via Pointwise Equality
Informal description
Let $s_1$ and $s_2$ be two $n$-dimensional simplices in an affine space over a field $k$. If for every index $i$ the corresponding points of $s_1$ and $s_2$ are equal (i.e., $s_1.\text{points}(i) = s_2.\text{points}(i)$), then $s_1 = s_2$.
Affine.Simplex.face definition
{n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : #fs = m + 1) : Simplex k P m
Full source 
/-- A face of a simplex is a simplex with the given subset of
points. -/
def face {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : #fs = m + 1) :
    Simplex k P m :=
  ⟨s.points ∘ fs.orderEmbOfFin h, s.independent.comp_embedding (fs.orderEmbOfFin h).toEmbedding⟩
Face of a simplex
Informal description
Given a simplex $s$ in an affine space over a field $k$, consisting of $n + 1$ affinely independent points, and a subset $fs$ of the indices of these points with cardinality $m + 1$, the face of $s$ corresponding to $fs$ is a new simplex of dimension $m$ formed by the points of $s$ indexed by $fs$.
Affine.Simplex.face_points theorem
{n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : #fs = m + 1) (i : Fin (m + 1)) : (s.face h).points i = s.points (fs.orderEmbOfFin h i)
Full source 
/-- The points of a face of a simplex are given by `mono_of_fin`. -/
theorem face_points {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ}
    (h : #fs = m + 1) (i : Fin (m + 1)) :
    (s.face h).points i = s.points (fs.orderEmbOfFin h i) :=
  rfl
Points of a Face Simplex via Order Embedding
Informal description
Let $s$ be an $n$-dimensional simplex in an affine space over a field $k$, consisting of $n+1$ affinely independent points. Given a subset $fs$ of the indices of these points with cardinality $m+1$, and an index $i$ in the face simplex, the $i$-th point of the face simplex is equal to the point of $s$ indexed by the $i$-th element of $fs$ under the order embedding determined by $h$.
Affine.Simplex.face_points' theorem
{n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : #fs = m + 1) : (s.face h).points = s.points ∘ fs.orderEmbOfFin h
Full source 
/-- The points of a face of a simplex are given by `mono_of_fin`. -/
theorem face_points' {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ}
    (h : #fs = m + 1) : (s.face h).points = s.points ∘ fs.orderEmbOfFin h :=
  rfl
Points of a Face Simplex as Restriction of Original Points
Informal description
Let $s$ be an $n$-dimensional simplex in an affine space over a field $k$, consisting of $n+1$ affinely independent points. Given a subset $fs$ of the indices of these points with cardinality $m+1$, the points of the corresponding face simplex $s.face$ are obtained by composing the original points function $s.points$ with the order embedding $fs.orderEmbOfFin$ that maps the indices of the face to the original simplex indices. In other words, the points of the face simplex are the restriction of the original simplex's points to the subset of indices specified by $fs$.
Affine.Simplex.face_eq_mkOfPoint theorem
{n : ℕ} (s : Simplex k P n) (i : Fin (n + 1)) : s.face (Finset.card_singleton i) = mkOfPoint k (s.points i)
Full source 
/-- A single-point face equals the 0-simplex constructed with
`mkOfPoint`. -/
@[simp]
theorem face_eq_mkOfPoint {n : ℕ} (s : Simplex k P n) (i : Fin (n + 1)) :
    s.face (Finset.card_singleton i) = mkOfPoint k (s.points i) := by
  ext
  simp [Affine.Simplex.mkOfPoint_points, Affine.Simplex.face_points, Finset.orderEmbOfFin_singleton]
Singleton Face of Simplex Equals Point Simplex
Informal description
Let $s$ be an $n$-dimensional simplex in an affine space over a field $k$, and let $i$ be an index in $\text{Fin}(n + 1)$. Then the face of $s$ corresponding to the singleton set $\{i\}$ is equal to the $0$-simplex constructed from the point $s.\text{points}(i)$.
Affine.Simplex.range_face_points theorem
{n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : #fs = m + 1) : Set.range (s.face h).points = s.points '' ↑fs
Full source 
/-- The set of points of a face. -/
@[simp]
theorem range_face_points {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ}
    (h : #fs = m + 1) : Set.range (s.face h).points = s.points '' ↑fs := by
  rw [face_points', Set.range_comp, Finset.range_orderEmbOfFin]
Range of Face Points Equals Image of Selected Indices
Informal description
Let $s$ be an $n$-dimensional simplex in an affine space over a field $k$, consisting of $n+1$ affinely independent points. Given a subset $fs$ of the indices of these points with cardinality $m+1$, the range of the points of the corresponding face simplex $s.face$ is equal to the image of $fs$ under the points function of $s$. In other words, the points of the face simplex are exactly those points of $s$ whose indices belong to $fs$. Mathematically, this can be expressed as: \[ \text{range } (s.face\ h).points = s.points \text{'' } fs \] where $h$ is a proof that the cardinality of $fs$ is $m+1$.
Affine.Simplex.faceOpposite definition
{n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) : Simplex k P (n - 1)
Full source 
/-- The face of a simplex with all but one point. -/
def faceOpposite {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) : Simplex k P (n - 1) :=
  s.face (fs := {j | j ≠ i}) (by simp [filter_ne', NeZero.one_le])
Opposite face of a simplex with respect to an index
Informal description
Given a simplex $s$ in an affine space over a field $k$ with $n + 1$ affinely independent points (where $n$ is nonzero), and an index $i$ of one of these points, the opposite face of $s$ with respect to $i$ is the simplex formed by all points of $s$ except the one at index $i$. This results in a simplex of dimension $n - 1$.
Affine.Simplex.range_faceOpposite_points theorem
{n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) : Set.range (s.faceOpposite i).points = s.points '' {j | j ≠ i}
Full source 
@[simp] lemma range_faceOpposite_points {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) :
    Set.range (s.faceOpposite i).points = s.points '' {j | j ≠ i} := by
  simp [faceOpposite]
Range of Opposite Face Points Equals Image of Non-Indexed Points
Informal description
Let $s$ be an $n$-dimensional simplex in an affine space over a field $k$, consisting of $n+1$ affinely independent points (where $n$ is nonzero). For any index $i$ of these points, the range of the points of the opposite face simplex $s.\text{faceOpposite}(i)$ is equal to the image under $s.\text{points}$ of all indices $j$ different from $i$. Mathematically, this can be expressed as: \[ \text{range } (s.\text{faceOpposite}(i)).\text{points} = s.\text{points} \text{'' } \{j \mid j \neq i\} \]
Affine.Simplex.mem_affineSpan_range_face_points_iff theorem
[Nontrivial k] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : #fs = m + 1) {i : Fin (n + 1)} : s.points i ∈ affineSpan k (Set.range (s.face h).points) ↔ i ∈ fs
Full source 
lemma mem_affineSpan_range_face_points_iff [Nontrivial k] {n : ℕ} (s : Simplex k P n)
    {fs : Finset (Fin (n + 1))} {m : ℕ} (h : #fs = m + 1) {i : Fin (n + 1)} :
    s.points i ∈ affineSpan k (Set.range (s.face h).points)s.points i ∈ affineSpan k (Set.range (s.face h).points) ↔ i ∈ fs := by
  rw [range_face_points, s.independent.mem_affineSpan_iff, mem_coe]
Characterization of Vertex Membership in Face Affine Span for Simplex
Informal description
Let $k$ be a nontrivial ring and $P$ an affine space over $k$. Given an $n$-dimensional simplex $s$ in $P$ with affinely independent vertices $\{p_0, \dots, p_n\}$, a subset $fs$ of the vertex indices with cardinality $m+1$, and an index $i \in \{0, \dots, n\}$, the vertex $p_i$ lies in the affine span of the face determined by $fs$ if and only if $i$ belongs to $fs$. More formally: \[ p_i \in \text{affineSpan}_k(\{p_j \mid j \in fs\}) \iff i \in fs \] where $h$ is a proof that $|fs| = m + 1$.
Affine.Simplex.mem_affineSpan_range_faceOpposite_points_iff theorem
[Nontrivial k] {n : ℕ} [NeZero n] (s : Simplex k P n) {i j : Fin (n + 1)} : s.points i ∈ affineSpan k (Set.range (s.faceOpposite j).points) ↔ i ≠ j
Full source 
lemma mem_affineSpan_range_faceOpposite_points_iff [Nontrivial k] {n : ℕ} [NeZero n]
    (s : Simplex k P n) {i j : Fin (n + 1)} :
    s.points i ∈ affineSpan k (Set.range (s.faceOpposite j).points)s.points i ∈ affineSpan k (Set.range (s.faceOpposite j).points) ↔ i ≠ j := by
  rw [faceOpposite, mem_affineSpan_range_face_points_iff]
  simp
Vertex Membership in Opposite Face Affine Span for Simplex
Informal description
Let $k$ be a nontrivial ring and $P$ an affine space over $k$. Given an $n$-dimensional simplex $s$ in $P$ with $n+1$ affinely independent points (where $n$ is nonzero) and indices $i,j \in \{0,\dots,n\}$, the point $p_i$ lies in the affine span of the points of the face opposite to $p_j$ if and only if $i \neq j$. More formally: \[ p_i \in \text{affineSpan}_k(\{p_k \mid k \neq j\}) \iff i \neq j \]
Affine.Simplex.reindex definition
{m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) : Simplex k P n
Full source 
/-- Remap a simplex along an `Equiv` of index types. -/
@[simps]
def reindex {m n : ℕ} (s : Simplex k P m) (e : FinFin (m + 1) ≃ Fin (n + 1)) : Simplex k P n :=
  ⟨s.points ∘ e.symm, (affineIndependent_equiv e.symm).2 s.independent⟩
Reindexing of a simplex via an equivalence
Informal description
Given a simplex $s$ in an affine space over a field $k$ with $m+1$ points and an equivalence $e$ between the index sets $\text{Fin}(m+1)$ and $\text{Fin}(n+1)$, the reindexed simplex $s.\text{reindex}\ e$ is a simplex with $n+1$ points obtained by composing the points of $s$ with the inverse of $e$. The affine independence of the points is preserved under this reindexing.
Affine.Simplex.reindex_refl theorem
{n : ℕ} (s : Simplex k P n) : s.reindex (Equiv.refl (Fin (n + 1))) = s
Full source 
/-- Reindexing by `Equiv.refl` yields the original simplex. -/
@[simp]
theorem reindex_refl {n : ℕ} (s : Simplex k P n) : s.reindex (Equiv.refl (Fin (n + 1))) = s :=
  ext fun _ => rfl
Reindexing a Simplex by the Identity Equivalence Preserves the Simplex
Informal description
For any $n$-dimensional simplex $s$ in an affine space over a field $k$, reindexing $s$ by the identity equivalence on the index set $\text{Fin}(n+1)$ yields $s$ itself, i.e., $s.\text{reindex}\ (\text{Equiv.refl}\ \text{Fin}(n+1)) = s$.
Affine.Simplex.reindex_trans theorem
{n₁ n₂ n₃ : ℕ} (e₁₂ : Fin (n₁ + 1) ≃ Fin (n₂ + 1)) (e₂₃ : Fin (n₂ + 1) ≃ Fin (n₃ + 1)) (s : Simplex k P n₁) : s.reindex (e₁₂.trans e₂₃) = (s.reindex e₁₂).reindex e₂₃
Full source 
/-- Reindexing by the composition of two equivalences is the same as reindexing twice. -/
@[simp]
theorem reindex_trans {n₁ n₂ n₃ : ℕ} (e₁₂ : FinFin (n₁ + 1) ≃ Fin (n₂ + 1))
    (e₂₃ : FinFin (n₂ + 1) ≃ Fin (n₃ + 1)) (s : Simplex k P n₁) :
    s.reindex (e₁₂.trans e₂₃) = (s.reindex e₁₂).reindex e₂₃ :=
  rfl
Composition Law for Simplex Reindexing
Informal description
Let $k$ be a field and $P$ an affine space over $k$. For natural numbers $n_1, n_2, n_3$, let $e_{12} : \text{Fin}(n_1 + 1) \simeq \text{Fin}(n_2 + 1)$ and $e_{23} : \text{Fin}(n_2 + 1) \simeq \text{Fin}(n_3 + 1)$ be equivalences between finite index sets, and let $s$ be an $n_1$-dimensional simplex in $P$. Then reindexing $s$ by the composition $e_{12} \circ e_{23}$ is equal to first reindexing $s$ by $e_{12}$ and then reindexing the result by $e_{23}$.
Affine.Simplex.reindex_reindex_symm theorem
{m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) : (s.reindex e).reindex e.symm = s
Full source 
/-- Reindexing by an equivalence and its inverse yields the original simplex. -/
@[simp]
theorem reindex_reindex_symm {m n : ℕ} (s : Simplex k P m) (e : FinFin (m + 1) ≃ Fin (n + 1)) :
    (s.reindex e).reindex e.symm = s := by rw [← reindex_trans, Equiv.self_trans_symm, reindex_refl]
Inverse Reindexing Recovers Original Simplex
Informal description
Let $k$ be a field and $P$ an affine space over $k$. For natural numbers $m$ and $n$, let $s$ be an $m$-dimensional simplex in $P$ and $e : \text{Fin}(m+1) \simeq \text{Fin}(n+1)$ be an equivalence between finite index sets. Then reindexing $s$ by $e$ and then reindexing the result by the inverse equivalence $e^{-1}$ yields the original simplex $s$, i.e., $(s.\text{reindex}\ e).\text{reindex}\ e^{-1} = s$.
Affine.Simplex.reindex_symm_reindex theorem
{m n : ℕ} (s : Simplex k P m) (e : Fin (n + 1) ≃ Fin (m + 1)) : (s.reindex e.symm).reindex e = s
Full source 
/-- Reindexing by the inverse of an equivalence and that equivalence yields the original simplex. -/
@[simp]
theorem reindex_symm_reindex {m n : ℕ} (s : Simplex k P m) (e : FinFin (n + 1) ≃ Fin (m + 1)) :
    (s.reindex e.symm).reindex e = s := by rw [← reindex_trans, Equiv.symm_trans_self, reindex_refl]
Inverse Reindexing Yields Original Simplex: $(s \circ e^{-1}) \circ e = s$
Informal description
Let $k$ be a field and $P$ an affine space over $k$. For natural numbers $m, n$, let $s$ be an $m$-dimensional simplex in $P$ and $e \colon \text{Fin}(n+1) \simeq \text{Fin}(m+1)$ be an equivalence between finite index sets. Then reindexing $s$ by the inverse equivalence $e^{-1}$ followed by reindexing with $e$ yields the original simplex $s$, i.e., $(s.\text{reindex}\ e^{-1}).\text{reindex}\ e = s$.
Affine.Simplex.reindex_range_points theorem
{m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) : Set.range (s.reindex e).points = Set.range s.points
Full source 
/-- Reindexing a simplex produces one with the same set of points. -/
@[simp]
theorem reindex_range_points {m n : ℕ} (s : Simplex k P m) (e : FinFin (m + 1) ≃ Fin (n + 1)) :
    Set.range (s.reindex e).points = Set.range s.points := by
  rw [reindex, Set.range_comp, Equiv.range_eq_univ, Set.image_univ]
Range Preservation under Simplex Reindexing
Informal description
Let $s$ be a simplex in an affine space over a field $k$ with $m+1$ points, and let $e \colon \text{Fin}(m+1) \simeq \text{Fin}(n+1)$ be an equivalence between finite index sets. Then the range of points of the reindexed simplex $s.\text{reindex}\ e$ is equal to the range of points of the original simplex $s$, i.e., $\text{range}((s.\text{reindex}\ e).\text{points}) = \text{range}(s.\text{points})$.
Affine.Simplex.face_centroid_eq_centroid theorem
{n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : #fs = m + 1) : Finset.univ.centroid k (s.face h).points = fs.centroid k s.points
Full source 
/-- The centroid of a face of a simplex as the centroid of a subset of
the points. -/
@[simp]
theorem face_centroid_eq_centroid {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ}
    (h : #fs = m + 1) : Finset.univ.centroid k (s.face h).points = fs.centroid k s.points := by
  convert (Finset.univ.centroid_map k (fs.orderEmbOfFin h).toEmbedding s.points).symm
  rw [← Finset.coe_inj, Finset.coe_map, Finset.coe_univ, Set.image_univ]
  simp
Centroid of a Simplex Face Equals Centroid of Corresponding Point Subset
Informal description
Let $s$ be an $n$-dimensional simplex in an affine space over a field $k$, consisting of $n+1$ affinely independent points. Given a subset $fs$ of the indices of these points with cardinality $m+1$, the centroid of the face of $s$ corresponding to $fs$ is equal to the centroid of the points of $s$ indexed by $fs$. More precisely, if $h$ is a proof that the cardinality of $fs$ is $m+1$, then the centroid of the points of the face simplex $s.\text{face}\,h$ (which is an $m$-dimensional simplex) is equal to the centroid of the points of $s$ indexed by $fs$.
Affine.Simplex.centroid_eq_iff theorem
[CharZero k] {n : ℕ} (s : Simplex k P n) {fs₁ fs₂ : Finset (Fin (n + 1))} {m₁ m₂ : ℕ} (h₁ : #fs₁ = m₁ + 1) (h₂ : #fs₂ = m₂ + 1) : fs₁.centroid k s.points = fs₂.centroid k s.points ↔ fs₁ = fs₂
Full source 
/-- Over a characteristic-zero division ring, the centroids given by
two subsets of the points of a simplex are equal if and only if those
faces are given by the same subset of points. -/
@[simp]
theorem centroid_eq_iff [CharZero k] {n : ℕ} (s : Simplex k P n) {fs₁ fs₂ : Finset (Fin (n + 1))}
    {m₁ m₂ : ℕ} (h₁ : #fs₁ = m₁ + 1) (h₂ : #fs₂ = m₂ + 1) :
    fs₁.centroid k s.points = fs₂.centroid k s.points ↔ fs₁ = fs₂ := by
  refine ⟨fun h => ?_, @congrArg _ _ fs₁ fs₂ (fun z => Finset.centroid k z s.points)⟩
  rw [Finset.centroid_eq_affineCombination_fintype,
    Finset.centroid_eq_affineCombination_fintype] at h
  have ha :=
    (affineIndependent_iff_indicator_eq_of_affineCombination_eq k s.points).1 s.independent _ _ _ _
      (fs₁.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one k h₁)
      (fs₂.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one k h₂) h
  simp_rw [Finset.coe_univ, Set.indicator_univ, funext_iff,
    Finset.centroidWeightsIndicator_def, Finset.centroidWeights, h₁, h₂] at ha
  ext i
  specialize ha i
  have key : ∀ n : ℕ, (n : k) + 1 ≠ 0 := fun n h => by norm_cast at h
  -- we should be able to golf this to
  -- `refine ⟨fun hi ↦ decidable.by_contradiction (fun hni ↦ ?_), ...⟩`,
  -- but for some unknown reason it doesn't work.
  constructor <;> intro hi <;> by_contra hni
  · simp [hni, hi, key] at ha
  · simpa [hni, hi, key] using ha.symm
Centroid Equality Characterizes Subset Equality in a Simplex over Characteristic Zero Division Ring
Informal description
Let $k$ be a division ring of characteristic zero, and let $s$ be an $n$-dimensional simplex in an affine space over $k$ with affinely independent points. For any two subsets $fs_1$ and $fs_2$ of the indices of the points of $s$, with cardinalities $m_1 + 1$ and $m_2 + 1$ respectively, the centroids of the points indexed by $fs_1$ and $fs_2$ are equal if and only if $fs_1 = fs_2$.
Affine.Simplex.face_centroid_eq_iff theorem
[CharZero k] {n : ℕ} (s : Simplex k P n) {fs₁ fs₂ : Finset (Fin (n + 1))} {m₁ m₂ : ℕ} (h₁ : #fs₁ = m₁ + 1) (h₂ : #fs₂ = m₂ + 1) : Finset.univ.centroid k (s.face h₁).points = Finset.univ.centroid k (s.face h₂).points ↔ fs₁ = fs₂
Full source 
/-- Over a characteristic-zero division ring, the centroids of two
faces of a simplex are equal if and only if those faces are given by
the same subset of points. -/
theorem face_centroid_eq_iff [CharZero k] {n : ℕ} (s : Simplex k P n)
    {fs₁ fs₂ : Finset (Fin (n + 1))} {m₁ m₂ : ℕ} (h₁ : #fs₁ = m₁ + 1) (h₂ : #fs₂ = m₂ + 1) :
    Finset.univFinset.univ.centroid k (s.face h₁).points = Finset.univ.centroid k (s.face h₂).points ↔
      fs₁ = fs₂ := by
  rw [face_centroid_eq_centroid, face_centroid_eq_centroid]
  exact s.centroid_eq_iff h₁ h₂
Equality of Face Centroids in a Simplex over Characteristic Zero Division Ring Characterizes Subset Equality
Informal description
Let $k$ be a division ring of characteristic zero, and let $s$ be an $n$-dimensional simplex in an affine space over $k$ with affinely independent points. For any two subsets $fs_1$ and $fs_2$ of the indices of the points of $s$, with cardinalities $m_1 + 1$ and $m_2 + 1$ respectively, the centroids of the corresponding faces of $s$ are equal if and only if $fs_1 = fs_2$. More precisely, if $h_1$ and $h_2$ are proofs that the cardinalities of $fs_1$ and $fs_2$ are $m_1 + 1$ and $m_2 + 1$ respectively, then the centroid of the points of the face simplex $s.\text{face}\,h_1$ is equal to the centroid of the points of the face simplex $s.\text{face}\,h_2$ if and only if $fs_1 = fs_2$.
Affine.Simplex.centroid_eq_of_range_eq theorem
{n : ℕ} {s₁ s₂ : Simplex k P n} (h : Set.range s₁.points = Set.range s₂.points) : Finset.univ.centroid k s₁.points = Finset.univ.centroid k s₂.points
Full source 
/-- Two simplices with the same points have the same centroid. -/
theorem centroid_eq_of_range_eq {n : ℕ} {s₁ s₂ : Simplex k P n}
    (h : Set.range s₁.points = Set.range s₂.points) :
    Finset.univ.centroid k s₁.points = Finset.univ.centroid k s₂.points := by
  rw [← Set.image_univ, ← Set.image_univ, ← Finset.coe_univ] at h
  exact
    Finset.univ.centroid_eq_of_inj_on_of_image_eq k _
      (fun _ _ _ _ he => AffineIndependent.injective s₁.independent he)
      (fun _ _ _ _ he => AffineIndependent.injective s₂.independent he) h
Centroid Equality for Simplices with Identical Point Ranges
Informal description
For any two $n$-dimensional simplices $s_1$ and $s_2$ in an affine space over a field $k$, if the ranges of their point sets are equal (i.e., $\text{range}(s_1.\text{points}) = \text{range}(s_2.\text{points})$), then their centroids coincide.
Affine.Simplex.interior definition
{n : ℕ} (s : Simplex k P n) : Set P
Full source 
/-- The interior of a simplex is the set of points that can be expressed as an affine combination
of the vertices with weights strictly between 0 and 1. This is equivalent to the intrinsic
interior of the convex hull of the vertices. -/
protected def interior {n : ℕ} (s : Simplex k P n) : Set P :=
  {p | ∃ w : Fin (n + 1) → k,
    (∑ i, w i = 1) ∧ (∀ i, w i ∈ Set.Ioo 0 1) ∧ Finset.univ.affineCombination k s.points w = p}
Interior of a simplex
Informal description
The interior of a simplex $s$ in an affine space over a field $k$ is the set of points $p$ that can be expressed as an affine combination of the vertices of $s$ with weights $w_i$ strictly between 0 and 1 (i.e., $w_i \in (0,1)$ for all $i$) and summing to 1 ($\sum_i w_i = 1$).
Affine.Simplex.affineCombination_mem_interior_iff theorem
{n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k} (hw : ∑ i, w i = 1) : Finset.univ.affineCombination k s.points w ∈ s.interior ↔ ∀ i, w i ∈ Set.Ioo 0 1
Full source 
lemma affineCombination_mem_interior_iff {n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k}
    (hw : ∑ i, w i = 1) :
    Finset.univFinset.univ.affineCombination k s.points w ∈ s.interiorFinset.univ.affineCombination k s.points w ∈ s.interior ↔ ∀ i, w i ∈ Set.Ioo 0 1 := by
  refine ⟨fun ⟨w', hw', hw'01, hww'⟩ ↦ ?_, fun h ↦ ⟨w, hw, h, rfl⟩⟩
  simp_rw [← (affineIndependent_iff_eq_of_fintype_affineCombination_eq k s.points).1
    s.independent w' w hw' hw hww']
  exact hw'01
Characterization of Interior Points via Affine Combination Weights in a Simplex
Informal description
Let $s$ be an $n$-dimensional simplex in an affine space over a field $k$, and let $w \colon \mathrm{Fin}(n+1) \to k$ be a weight function such that $\sum_{i} w_i = 1$. The affine combination $\sum_{i} w_i s_i$ (where $s_i$ are the vertices of $s$) lies in the interior of $s$ if and only if all weights $w_i$ satisfy $0 < w_i < 1$.
Affine.Simplex.closedInterior definition
{n : ℕ} (s : Simplex k P n) : Set P
Full source 
/-- `s.closedInterior` is the set of points that can be expressed as an affine combination
of the vertices with weights between 0 and 1 inclusive. This is equivalent to the convex hull of
the vertices or the closure of the interior. -/
protected def closedInterior {n : ℕ} (s : Simplex k P n) : Set P :=
  {p | ∃ w : Fin (n + 1) → k,
    (∑ i, w i = 1) ∧ (∀ i, w i ∈ Set.Icc 0 1) ∧ Finset.univ.affineCombination k s.points w = p}
Closed interior of a simplex (convex hull of vertices)
Informal description
For an $n$-dimensional simplex $s$ in an affine space over a field $k$, the set $\text{closedInterior}(s)$ consists of all points $p$ that can be expressed as an affine combination of the vertices of $s$ with weights $w_i$ (for $i = 1, \ldots, n+1$) satisfying $\sum_i w_i = 1$ and $0 \leq w_i \leq 1$ for all $i$. In other words, $\text{closedInterior}(s)$ is the convex hull of the vertices of $s$, or equivalently, the closure of the interior of $s$.
Affine.Simplex.affineCombination_mem_closedInterior_iff theorem
{n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k} (hw : ∑ i, w i = 1) : Finset.univ.affineCombination k s.points w ∈ s.closedInterior ↔ ∀ i, w i ∈ Set.Icc 0 1
Full source 
lemma affineCombination_mem_closedInterior_iff {n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k}
    (hw : ∑ i, w i = 1) :
    Finset.univFinset.univ.affineCombination k s.points w ∈ s.closedInteriorFinset.univ.affineCombination k s.points w ∈ s.closedInterior ↔ ∀ i, w i ∈ Set.Icc 0 1 := by
  refine ⟨fun ⟨w', hw', hw'01, hww'⟩ ↦ ?_, fun h ↦ ⟨w, hw, h, rfl⟩⟩
  simp_rw [← (affineIndependent_iff_eq_of_fintype_affineCombination_eq k s.points).1
    s.independent w' w hw' hw hww']
  exact hw'01
Characterization of Points in the Closed Interior of a Simplex via Affine Combinations
Informal description
Let $s$ be an $n$-dimensional simplex in an affine space over a field $k$, and let $w \colon \mathrm{Fin}(n+1) \to k$ be a weight function such that $\sum_{i} w_i = 1$. Then the affine combination $\sum_{i} w_i s_i$ lies in the closed interior (convex hull) of $s$ if and only if each weight $w_i$ satisfies $0 \leq w_i \leq 1$.