mathlib3 documentation

linear_algebra.affine_space.independent

Affine independence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines affinely independent families of points.

Main definitions #

References #

source
def affine_independent (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} (p : ι → P) :
Prop

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

Equations
source
theorem affine_independent_def (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} (p : ι → P) :
affine_independent k p ↔ ∀ (s : finset ι) (w : ι → k), s.sum (λ (i : ι), w i) = 0 → ⇑(s.weighted_vsub p) w = 0 → ∀ (i : ι), i ∈ s → w i = 0

The definition of affine_independent.

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

A family with at most one point is affinely independent.

source
theorem affine_independent_iff_of_fintype (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} [fintype ι] (p : ι → P) :
affine_independent k p ↔ ∀ (w : ι → k), finset.univ.sum (λ (i : ι), w i) = 0 → ⇑(finset.univ.weighted_vsub p) w = 0 → ∀ (i : ι), w i = 0

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

source
theorem affine_independent_iff_linear_independent_vsub (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} (p : ι → P) (i1 : ι) :
affine_independent k p ↔ linear_independent k (λ (i : {x // x ≠ i1}), p ↑i -ᵥ p i1)

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

source
theorem affine_independent_set_iff_linear_independent_vsub (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} {p₁ : P} (hp₁ : p₁ ∈ s) :
affine_independent k (λ (p : ↥s), ↑p) ↔ linear_independent k (λ (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.

source
theorem linear_independent_set_iff_affine_independent_vadd_union_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set V} (hs : ∀ (v : V), v ∈ s → v ≠ 0) (p₁ : P) :
linear_independent k (λ (v : ↥s), ↑v) ↔ affine_independent k (λ (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.

source
theorem affine_independent_iff_indicator_eq_of_affine_combination_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} (p : ι → P) :
affine_independent k p ↔ ∀ (s1 s2 : finset ι) (w1 w2 : ι → k), s1.sum (λ (i : ι), w1 i) = 1 → s2.sum (λ (i : ι), w2 i) = 1 → ⇑(finset.affine_combination k s1 p) w1 = ⇑(finset.affine_combination k s2 p) w2 → ↑s1.indicator w1 = ↑s2.indicator w2

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

source
theorem affine_independent_iff_eq_of_fintype_affine_combination_eq (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} [fintype ι] (p : ι → P) :
affine_independent k p ↔ ∀ (w1 w2 : ι → k), finset.univ.sum (λ (i : ι), w1 i) = 1 → finset.univ.sum (λ (i : ι), w2 i) = 1 → ⇑(finset.affine_combination k finset.univ p) w1 = ⇑(finset.affine_combination k finset.univ p) w2 → w1 = w2

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

source
theorem affine_independent.units_line_map {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {p : ι → P} (hp : affine_independent k p) (j : ι) (w : ι → kˣ) :
affine_independent k (λ (i : ι), ⇑(affine_map.line_map (p j) (p i)) ↑(w i))

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

This is the affine version of linear_independent.units_smul.

source
theorem affine_independent.indicator_eq_of_affine_combination_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {p : ι → P} (ha : affine_independent k p) (s₁ s₂ : finset ι) (w₁ w₂ : ι → k) (hw₁ : s₁.sum (λ (i : ι), w₁ i) = 1) (hw₂ : s₂.sum (λ (i : ι), w₂ i) = 1) (h : ⇑(finset.affine_combination k s₁ p) w₁ = ⇑(finset.affine_combination k s₂ p) w₂) :
↑s₁.indicator w₁ = ↑s₂.indicator w₂
source
@[protected]
theorem affine_independent.injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : affine_independent k p) :
function.injective p

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

source
theorem affine_independent.comp_embedding {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {ι2 : Type u_5} (f : ι2 ↪ ι) {p : ι → P} (ha : affine_independent k p) :
affine_independent k (p ∘ ⇑f)

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

source
@[protected]
theorem affine_independent.subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {p : ι → P} (ha : affine_independent k p) (s : set ι) :
affine_independent k (λ (i : ↥s), p ↑i)

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

source
@[protected]
theorem affine_independent.range {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {p : ι → P} (ha : affine_independent k p) :
affine_independent k (λ (x : ↥(set.range p)), ↑x)

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

source
theorem affine_independent_equiv {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') {p : ι' → P} :
affine_independent k (p ∘ ⇑e) ↔ affine_independent k p
source
@[protected]
theorem affine_independent.mono {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {s t : set P} (ha : affine_independent k (λ (x : ↥t), ↑x)) (hs : s ⊆ t) :
affine_independent k (λ (x : ↥s), ↑x)

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

source
theorem affine_independent.of_set_of_injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {p : ι → P} (ha : affine_independent k (λ (x : ↥(set.range p)), ↑x)) (hi : function.injective p) :
affine_independent k p

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

source
theorem affine_independent.of_comp {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {p : ι → P} (f : P →ᵃ[k] P₂) (hai : affine_independent k (⇑f ∘ p)) :
affine_independent k p

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

source
theorem affine_independent.map' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {p : ι → P} (hai : affine_independent k p) (f : P →ᵃ[k] P₂) (hf : function.injective ⇑f) :
affine_independent k (⇑f ∘ p)

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

source
theorem affine_map.affine_independent_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {p : ι → P} (f : P →ᵃ[k] P₂) (hf : function.injective ⇑f) :
affine_independent k (⇑f ∘ p) ↔ affine_independent k p

Injective affine maps preserve affine independence.

source
theorem affine_equiv.affine_independent_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {p : ι → P} (e : P ≃ᵃ[k] P₂) :
affine_independent k (⇑e ∘ p) ↔ affine_independent k p

Affine equivalences preserve affine independence of families of points.

source
theorem affine_equiv.affine_independent_set_of_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {V₂ : Type u_5} {P₂ : Type u_6} [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] {s : set P} (e : P ≃ᵃ[k] P₂) :
affine_independent k coe ↔ affine_independent k coe

Affine equivalences preserve affine independence of subsets.

source
theorem affine_independent.exists_mem_inter_of_exists_mem_inter_affine_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : affine_independent k p) {s1 s2 : set ι} {p0 : P} (hp0s1 : p0 ∈ affine_span k (p '' s1)) (hp0s2 : p0 ∈ affine_span k (p '' s2)) :
∃ (i : ι), i ∈ s1 ∩ s2

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

source
theorem affine_independent.affine_span_disjoint_of_disjoint {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : affine_independent k p) {s1 s2 : set ι} (hd : disjoint s1 s2) :
disjoint ↑(affine_span k (p '' s1)) ↑(affine_span k (p '' s2))

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

source
@[protected, simp]
theorem affine_independent.mem_affine_span_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : affine_independent k p) (i : ι) (s : set ι) :
p i ∈ affine_span k (p '' s) ↔ i ∈ s

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

source
theorem affine_independent.not_mem_affine_span_diff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} [nontrivial k] {p : ι → P} (ha : affine_independent k p) (i : ι) (s : set ι) :
p i ∉ affine_span k (p '' (s \ {i}))

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

source
theorem exists_nontrivial_relation_sum_zero_of_not_affine_ind {k : Type u_1} {V : Type u_2} [ring k] [add_comm_group V] [module k V] {t : finset V} (h : ¬affine_independent k coe) :
∃ (f : V → k), t.sum (λ (e : V), f e • e) = 0 ∧ t.sum (λ (e : V), f e) = 0 ∧ ∃ (x : V) (H : x ∈ t), f x ≠ 0
source
theorem affine_independent_iff {k : Type u_1} {V : Type u_2} [ring k] [add_comm_group V] [module k V] {ι : Type u_3} {p : ι → V} :
affine_independent k p ↔ ∀ (s : finset ι) (w : ι → k), s.sum w = 0 → s.sum (λ (e : ι), w e • p e) = 0 → ∀ (e : ι), e ∈ s → w e = 0

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

source
theorem weighted_vsub_mem_vector_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {p : ι → P} (h : affine_independent k p) {w w₁ w₂ : ι → k} {s : finset ι} (hw : s.sum (λ (i : ι), w i) = 0) (hw₁ : s.sum (λ (i : ι), w₁ i) = 1) (hw₂ : s.sum (λ (i : ι), w₂ i) = 1) :
⇑(s.weighted_vsub p) w ∈ vector_span k {⇑(finset.affine_combination k s p) w₁, ⇑(finset.affine_combination k s p) w₂} ↔ ∃ (r : k), ∀ (i : ι), i ∈ s → w i = r * (w₁ i - w₂ i)

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

source
theorem affine_combination_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {p : ι → P} (h : affine_independent k p) {w w₁ w₂ : ι → k} {s : finset ι} (hw : s.sum (λ (i : ι), w i) = 1) (hw₁ : s.sum (λ (i : ι), w₁ i) = 1) (hw₂ : s.sum (λ (i : ι), w₂ i) = 1) :
⇑(finset.affine_combination k s p) w ∈ affine_span k {⇑(finset.affine_combination k s p) w₁, ⇑(finset.affine_combination k s p) w₂} ↔ ∃ (r : k), ∀ (i : ι), i ∈ s → w i = r * (w₂ i - w₁ i) + w₁ i

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

source
theorem exists_subset_affine_independent_affine_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : set P} (h : affine_independent k (λ (p : ↥s), ↑p)) :
∃ (t : set P), s ⊆ t ∧ affine_independent k (λ (p : ↥t), ↑p) ∧ affine_span k t = ⊤

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

source
theorem exists_affine_independent (k : Type u_1) (V : Type u_2) {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] (s : set P) :
∃ (t : set P) (H : t ⊆ s), affine_span k t = affine_span k s ∧ affine_independent k coe
source
theorem affine_independent_of_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {p₁ p₂ : P} (h : p₁ ≠ p₂) :
affine_independent k ![p₁, p₂]

Two different points are affinely independent.

source
theorem affine_independent.affine_independent_of_not_mem_span {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {p : ι → P} {i : ι} (ha : affine_independent k (λ (x : {y // y ≠ i}), p ↑x)) (hi : p i ∉ affine_span k (p '' {x : ι | x ≠ i})) :
affine_independent k p

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

source
theorem affine_independent_of_ne_of_mem_of_mem_of_not_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p₁ p₂ p₃ : P} (hp₁p₂ : p₁ ≠ p₂) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∉ s) :
affine_independent k ![p₁, p₂, p₃]

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

source
theorem affine_independent_of_ne_of_mem_of_not_mem_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p₁ p₂ p₃ : P} (hp₁p₃ : p₁ ≠ p₃) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∉ s) (hp₃ : p₃ ∈ s) :
affine_independent k ![p₁, p₂, p₃]

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

source
theorem affine_independent_of_ne_of_not_mem_of_mem_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {s : affine_subspace k P} {p₁ p₂ p₃ : P} (hp₂p₃ : p₂ ≠ p₃) (hp₁ : p₁ ∉ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) :
affine_independent k ![p₁, p₂, p₃]

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

source
theorem sign_eq_of_affine_combination_mem_affine_span_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [linear_ordered_ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {p : ι → P} (h : affine_independent k p) {w w₁ w₂ : ι → k} {s : finset ι} (hw : s.sum (λ (i : ι), w i) = 1) (hw₁ : s.sum (λ (i : ι), w₁ i) = 1) (hw₂ : s.sum (λ (i : ι), w₂ i) = 1) (hs : ⇑(finset.affine_combination k s p) w ∈ affine_span k {⇑(finset.affine_combination k s p) w₁, ⇑(finset.affine_combination k s p) w₂}) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hi0 : w₁ i = 0) (hj0 : w₁ j = 0) (hij : ⇑sign (w₂ i) = ⇑sign (w₂ j)) :
⇑sign (w i) = ⇑sign (w j)

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

source
theorem sign_eq_of_affine_combination_mem_affine_span_single_line_map {k : Type u_1} {V : Type u_2} {P : Type u_3} [linear_ordered_ring k] [add_comm_group V] [module k V] [add_torsor V P] {ι : Type u_4} {p : ι → P} (h : affine_independent k p) {w : ι → k} {s : finset ι} (hw : s.sum (λ (i : ι), w i) = 1) {i₁ i₂ i₃ : ι} (h₁ : i₁ ∈ s) (h₂ : i₂ ∈ s) (h₃ : i₃ ∈ s) (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {c : k} (hc0 : 0 < c) (hc1 : c < 1) (hs : ⇑(finset.affine_combination k s p) w ∈ affine_span k {p i₁, ⇑(affine_map.line_map (p i₂) (p i₃)) c}) :
⇑sign (w i₂) = ⇑sign (w i₃)

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

source
structure affine.simplex (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [add_comm_group V] [module k V] [add_torsor V P] (n : ℕ) :
Type u_3

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

Instances for affine.simplex
source
@[reducible]
def affine.triangle (k : Type u_1) {V : Type u_2} (P : Type u_3) [ring k] [add_comm_group V] [module k V] [add_torsor V P] :
Type u_3

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

source
def affine.simplex.mk_of_point (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] (p : P) :
affine.simplex k P 0

Construct a 0-simplex from a point.

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

The point in a simplex constructed with mk_of_point.

source
@[protected, instance]
def affine.simplex.inhabited (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] [inhabited P] :
inhabited (affine.simplex k P 0)
Equations
source
@[protected, instance]
def affine.simplex.nonempty (k : Type u_1) {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] :
nonempty (affine.simplex k P 0)
source
@[ext]
theorem affine.simplex.ext {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {n : ℕ} {s1 s2 : affine.simplex k P n} (h : ∀ (i : fin (n + 1)), s1.points i = s2.points i) :
s1 = s2

Two simplices are equal if they have the same points.

source
theorem affine.simplex.ext_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {n : ℕ} (s1 s2 : affine.simplex k P 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.

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

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

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

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

source
theorem affine.simplex.face_points' {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {n : ℕ} (s : affine.simplex k P n) {fs : finset (fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) :
(s.face h).points = s.points ∘ ⇑(fs.order_emb_of_fin h)

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

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

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

source
@[simp]
theorem affine.simplex.range_face_points {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {n : ℕ} (s : affine.simplex k P n) {fs : finset (fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) :
set.range (s.face h).points = s.points '' ↑fs

The set of points of a face.

source
@[simp]
theorem affine.simplex.reindex_points {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {m n : ℕ} (s : affine.simplex k P m) (e : fin (m + 1) ≃ fin (n + 1)) (ᾰ : fin (n + 1)) :
(s.reindex e).points ᾰ = (s.points ∘ ⇑(e.symm)) ᾰ
source
def affine.simplex.reindex {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {m n : ℕ} (s : affine.simplex k P m) (e : fin (m + 1) ≃ fin (n + 1)) :
affine.simplex k P n

Remap a simplex along an equiv of index types.

Equations
source
@[simp]
theorem affine.simplex.reindex_refl {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {n : ℕ} (s : affine.simplex k P n) :
s.reindex (equiv.refl (fin (n + 1))) = s

Reindexing by equiv.refl yields the original simplex.

source
@[simp]
theorem affine.simplex.reindex_trans {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {n₁ n₂ n₃ : ℕ} (e₁₂ : fin (n₁ + 1) ≃ fin (n₂ + 1)) (e₂₃ : fin (n₂ + 1) ≃ fin (n₃ + 1)) (s : affine.simplex k P n₁) :
s.reindex (e₁₂.trans e₂₃) = (s.reindex e₁₂).reindex e₂₃

Reindexing by the composition of two equivalences is the same as reindexing twice.

source
@[simp]
theorem affine.simplex.reindex_reindex_symm {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {m n : ℕ} (s : affine.simplex k P m) (e : fin (m + 1) ≃ fin (n + 1)) :
(s.reindex e).reindex e.symm = s

Reindexing by an equivalence and its inverse yields the original simplex.

source
@[simp]
theorem affine.simplex.reindex_symm_reindex {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {m n : ℕ} (s : affine.simplex k P m) (e : fin (n + 1) ≃ fin (m + 1)) :
(s.reindex e.symm).reindex e = s

Reindexing by the inverse of an equivalence and that equivalence yields the original simplex.

source
@[simp]
theorem affine.simplex.reindex_range_points {k : Type u_1} {V : Type u_2} {P : Type u_3} [ring k] [add_comm_group V] [module k V] [add_torsor V P] {m n : ℕ} (s : affine.simplex k P m) (e : fin (m + 1) ≃ fin (n + 1)) :
set.range (s.reindex e).points = set.range s.points

Reindexing a simplex produces one with the same set of points.

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

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

source
@[simp]
theorem affine.simplex.centroid_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [char_zero k] {n : ℕ} (s : affine.simplex k P n) {fs₁ fs₂ : finset (fin (n + 1))} {m₁ m₂ : ℕ} (h₁ : fs₁.card = m₁ + 1) (h₂ : fs₂.card = m₂ + 1) :
finset.centroid k fs₁ s.points = finset.centroid k 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.

source
theorem affine.simplex.face_centroid_eq_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] [char_zero k] {n : ℕ} (s : affine.simplex k P n) {fs₁ fs₂ : finset (fin (n + 1))} {m₁ m₂ : ℕ} (h₁ : fs₁.card = m₁ + 1) (h₂ : fs₂.card = m₂ + 1) :
finset.centroid k finset.univ (s.face h₁).points = finset.centroid k finset.univ (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.

source
theorem affine.simplex.centroid_eq_of_range_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring k] [add_comm_group V] [module k V] [add_torsor V P] {n : ℕ} {s₁ s₂ : affine.simplex k P n} (h : set.range s₁.points = set.range s₂.points) :
finset.centroid k finset.univ s₁.points = finset.centroid k finset.univ s₂.points

Two simplices with the same points have the same centroid.