# mathlibdocumentation

linear_algebra.affine_space.independent

# Affine independence

This file defines affinely independent families of points.

## Main definitions

• affine_independent 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
def affine_independent (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} :
(ι → P) → Prop

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

Equations
theorem affine_independent_def (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} (p : ι → P) :
∀ (s : finset ι) (w : ι → k), ∑ (i : ι) in s, w i = 0(s.weighted_vsub p) w = 0∀ (i : ι), i sw i = 0

The definition of affine_independent.

theorem affine_independent_of_subsingleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} [subsingleton ι] (p : ι → P) :

A family with at most one point is affinely independent.

theorem affine_independent_iff_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} [fintype ι] (p : ι → P) :
∀ (w : ι → k), ∑ (i : ι), w i = 0 = 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.

theorem affine_independent_iff_linear_independent_vsub (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} (p : ι → P) (i1 : ι) :
(λ (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 affine_independent_set_iff_linear_independent_vsub (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : set P} {p₁ : P} :
p₁ s (λ (p : s), p) (λ (v : ((λ (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 linear_independent_set_iff_affine_independent_vadd_union_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s : set V} (hs : ∀ (v : V), v sv 0) (p₁ : P) :
(λ (v : s), v) (λ (p : ({p₁} (λ (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 affine_independent_iff_indicator_eq_of_affine_combination_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} (p : ι → P) :
∀ (s1 s2 : finset ι) (w1 w2 : ι → k), ∑ (i : ι) in s1, w1 i = 1∑ (i : ι) in s2, w2 i = 1(s1.affine_combination p) w1 = (s2.affine_combination p) w2s1.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 injective_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} [nontrivial k] {p : ι → P} :

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

theorem affine_independent_embedding_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} {ι2 : Type u_5} (f : ι2 ι) {p : ι → P} :
(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 affine_independent_subtype_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} {p : ι → P} (ha : p) (s : set ι) :
(λ (i : s), p i)

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

theorem affine_independent_set_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} {p : ι → P} :
(λ (x : (set.range p)), x)

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

theorem affine_independent_of_subset_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {s t : set P} :
(λ (x : t), x)s t (λ (x : s), x)

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

theorem affine_independent_of_affine_independent_set_of_injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} {p : ι → P} :
(λ (x : (set.range p)), x)

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

theorem exists_mem_inter_of_exists_mem_inter_affine_span_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : p) {s1 s2 : set ι} {p0 : P} :
p0 (p '' s1)p0 (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 affine_span_disjoint_of_disjoint_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : p) {s1 s2 : set ι} :
s1 s2 = (p '' s1)) (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 mem_affine_span_iff_mem_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : p) (i : ι) (s : set ι) :
p i (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 not_mem_affine_span_diff_of_affine_independent {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : p) (i : ι) (s : set ι) :
p i (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 exists_subset_affine_independent_affine_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {s : set P} :
(λ (p : s), p)(∃ (t : set P), s t (λ (p : t), p) t = )

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

theorem affine_independent_of_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [field k] [ V] [ P] {p₁ p₂ : P} :
p₁ p₂ ![p₁, p₂]

Two different points are affinely independent.

structure affine.simplex (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [ V] [ P] :
Type u_3
• points : fin (n + 1) → P
• independent :

A simplex k P n is a collection of n + 1 affinely independent points.

def affine.triangle (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [ V] [ P] :
Type u_3

A triangle k P is a collection of three affinely independent points.

def affine.simplex.mk_of_point (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] :
P → 0

Construct a 0-simplex from a point.

Equations
@[simp]
theorem affine.simplex.mk_of_point_points (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] (p : P) (i : fin 1) :
i = p

The point in a simplex constructed with mk_of_point.

@[instance]
def affine.simplex.inhabited (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] [inhabited P] :

Equations
@[instance]
def affine.simplex.nonempty (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] :

@[ext]
theorem affine.simplex.ext {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {n : } {s1 s2 : n} :
(∀ (i : fin (n + 1)), s1.points i = s2.points i)s1 = s2

Two simplices are equal if they have the same points.

theorem affine.simplex.ext_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {n : } (s1 s2 : n) :
s1 = s2 ∀ (i : fin (n + 1)), s1.points i = s2.points i

Two simplices are equal if and only if they have the same points.

def affine.simplex.face {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {n : } (s : n) {fs : finset (fin (n + 1))} {m : } :
fs.card = m + 1 m

A face of a simplex is a simplex with the given subset of points.

Equations
theorem affine.simplex.face_points {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {n : } (s : n) {fs : finset (fin (n + 1))} {m : } (h : fs.card = m + 1) (i : fin (m + 1)) :
(s.face h).points i = s.points (fs.mono_of_fin h i)

The points of a face of a simplex are given by mono_of_fin.

@[simp]
theorem affine.simplex.face_eq_mk_of_point {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {n : } (s : n) (i : fin (n + 1)) :
s.face _ = (s.points i)

A single-point face equals the 0-simplex constructed with mk_of_point.

@[simp]
theorem affine.simplex.range_face_points {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [ V] [ P] {n : } (s : n) {fs : finset (fin (n + 1))} {m : } (h : fs.card = m + 1) :

The set of points of a face.

@[simp]
theorem affine.simplex.face_centroid_eq_centroid {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] {n : } (s : n) {fs : finset (fin (n + 1))} {m : } (h : fs.card = m + 1) :
(s.face h).points = fs s.points

The centroid of a face of a simplex as the centroid of a subset of the points.

@[simp]
theorem affine.simplex.centroid_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] [char_zero k] {n : } (s : n) {fs₁ fs₂ : finset (fin (n + 1))} {m₁ m₂ : } :
fs₁.card = m₁ + 1fs₂.card = m₂ + 1 fs₁ s.points = fs₂ s.points fs₁ = fs₂)

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.

theorem affine.simplex.face_centroid_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] [char_zero k] {n : } (s : n) {fs₁ fs₂ : finset (fin (n + 1))} {m₁ m₂ : } (h₁ : fs₁.card = m₁ + 1) (h₂ : fs₂.card = m₂ + 1) :
(s.face h₁).points = (s.face h₂).points fs₁ = fs₂

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 affine.simplex.centroid_eq_of_range_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [ V] [ P] {n : } {s₁ s₂ : n} :
=

Two simplices with the same points have the same centroid.