affineIndependent_iff_of_fintype
theorem affineIndependent_iff_of_fintype :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : Fintype ι] (p : ι → P),
AffineIndependent k p ↔
∀ (w : ι → k), (Finset.univ.sum fun i => w i) = 0 → (Finset.univ.weightedVSub p) w = 0 → ∀ (i : ι), w i = 0
The theorem states that for a family of points 'p', indexed by a finite type 'ι', the family is affinely independent if and only if there is no nontrivial weighted subtraction over the universal finite set of type 'ι' (represented by `Finset.univ`) such that the sum of the weights is zero leading to a zero result of the weighted subtraction. In other words, if the sum of weights of all elements in the universal set is zero, and the weighted subtraction operation on the set of points also gives zero, then all the weights of the elements in the universal set must be zero. This condition is both necessary and sufficient for the family of points to be affinely independent.
More concisely: A family of points indexed by a finite type is affinely independent if and only if there does not exist a non-trivial set of weights for the universal finite set, summing to zero, such that the weighted subtraction of any two elements results in zero.
|
sign_eq_of_affineCombination_mem_affineSpan_pair
theorem sign_eq_of_affineCombination_mem_affineSpan_pair :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : LinearOrderedRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
AffineIndependent k p →
∀ {w w₁ w₂ : ι → k} {s : Finset ι},
(s.sum fun i => w i) = 1 →
(s.sum fun i => w₁ i) = 1 →
(s.sum fun i => w₂ i) = 1 →
(Finset.affineCombination k s p) w ∈
affineSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂} →
∀ {i j : ι},
i ∈ s →
j ∈ s →
w₁ i = 0 →
w₁ j = 0 →
SignType.sign (w₂ i) = SignType.sign (w₂ j) → SignType.sign (w i) = SignType.sign (w j)
The theorem `sign_eq_of_affineCombination_mem_affineSpan_pair` states that for a given affinely independent family of points, if an affine combination of these points lies within the affine span of two other affine combinations of these points, and if for two specific indices, the coefficients of the first point in the span are zero and the coefficients of the second point in the span have the same sign, then the coefficients of the combination that lies within the span will also have the same sign. Essentially, it expresses a relationship between the signs of the coefficients of points in an affine span under certain conditions.
More concisely: If two affine combinations of affinely independent points lie in the same affine span and have identical coefficients for two specific points with the same sign, then the coefficients of the third point in the combinations have the same sign.
|
sign_eq_of_affineCombination_mem_affineSpan_single_lineMap
theorem sign_eq_of_affineCombination_mem_affineSpan_single_lineMap :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : LinearOrderedRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
AffineIndependent k p →
∀ {w : ι → k} {s : Finset ι},
(s.sum fun i => w i) = 1 →
∀ {i₁ i₂ i₃ : ι},
i₁ ∈ s →
i₂ ∈ s →
i₃ ∈ s →
i₁ ≠ i₂ →
i₁ ≠ i₃ →
i₂ ≠ i₃ →
∀ {c : k},
0 < c →
c < 1 →
(Finset.affineCombination k s p) w ∈
affineSpan k {p i₁, (AffineMap.lineMap (p i₂) (p i₃)) c} →
SignType.sign (w i₂) = SignType.sign (w i₃)
This theorem states that given an affinely independent family of points, if an affine combination of these points lies in the affine span of a single point from this family and another point which is a combination of two other distinct points from this family, formed using `lineMap` with a coefficient between 0 and 1, then the coefficients of these two points used in the line map in the original affine combination have the same sign. This condition is established under the assumptions that the sum of the coefficients in the original affine combination is 1, and the three distinct points used are all in the index set for the original affine combination.
More concisely: Given an affinely independent family of points, if an affine combination of two distinct points from this family and a third point in the span of both have coefficients with the same sign in the original combination, then the third point is a convex combination of the two distinct points.
|
AffineIndependent.mem_affineSpan_iff
theorem AffineIndependent.mem_affineSpan_iff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : Nontrivial k] {p : ι → P},
AffineIndependent k p → ∀ (i : ι) (s : Set ι), p i ∈ affineSpan k (p '' s) ↔ i ∈ s
The theorem states that for a family of points which are affinely independent in a nontrivial ring, a given point within the family lies within the affine span of a set of points (this set is determined by a subset of the indices of the family of points) if and only if the index of that given point is included in the subset of the indices. This theorem establishes a direct correspondence between the membership of a point in the affine span and the membership of its index in the subset of indices.
More concisely: For a family of points in a nontrivial ring, a point is in the affine span of other points if and only if its index is in the indices of those points.
|
AffineIndependent.not_mem_affineSpan_diff
theorem AffineIndependent.not_mem_affineSpan_diff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : Nontrivial k] {p : ι → P},
AffineIndependent k p → ∀ (i : ι) (s : Set ι), p i ∉ affineSpan k (p '' (s \ {i}))
The theorem `AffineIndependent.not_mem_affineSpan_diff` states that, given a family of points that is affinely independent in an environment where the underlying ring is nontrivial, a specific point in that family does not lie in the affine span of the other points. More concretely, for any index `i` and any set `s` of indices, the point `p i` is not in the affine span of the points corresponding to the indices in `s` except for `i`. Affine independent means that no nontrivial weighted subtractions (where the sum of weights is 0) are 0. The affine span of a set of points is the smallest affine subspace containing those points.
More concisely: Given an affinely independent set of points in a nontrivial ring, no point in the set lies in the affine span of the other points except for itself.
|
affineIndependent_iff_eq_of_fintype_affineCombination_eq
theorem affineIndependent_iff_eq_of_fintype_affineCombination_eq :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : Fintype ι] (p : ι → P),
AffineIndependent k p ↔
∀ (w1 w2 : ι → k),
(Finset.univ.sum fun i => w1 i) = 1 →
(Finset.univ.sum fun i => w2 i) = 1 →
(Finset.affineCombination k Finset.univ p) w1 = (Finset.affineCombination k Finset.univ p) w2 → w1 = w2
The theorem states that a finite family of points is affinely independent if and only if, for any two affine combinations (where the sum of weights is 1) that evaluate to the same point, their weights are the same. In other words, if we have two sets of weights that sum to 1 and they're used to form affine combinations of the same set of points, and these combinations result in the same point, then the weights in each set must be exactly the same. This is a characteristic of affine independence.
More concisely: A finite set of points is affinely independent if and only if for all distinct pairs of affine combinations of these points with equal values, their weights are equal.
|
Affine.Simplex.face_eq_mkOfPoint
theorem Affine.Simplex.face_eq_mkOfPoint :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) (i : Fin (n + 1)),
s.face ⋯ = Affine.Simplex.mkOfPoint k (s.points i)
The theorem `Affine.Simplex.face_eq_mkOfPoint` states that for any ring `k`, additive commutative group `V`, module `V` over `k`, and additive torsor `P` over `V`, and for any natural number `n`, every single-point face of an n-simplex `s` is equivalent to a 0-simplex created from a single point of `s`. More simply, it says that if we take a simplex (a generalization of a triangle in any dimension), and we take a face of that simplex that consists of only a single point, then this face is equivalent to a 0-simplex (a point) created from that same point.
More concisely: For any ring `k`, additive commutative group `V`, module `V` over `k`, and additive torsor `P` over `V`, every single-point face of an `n`-simplex `s` in `P` is equivalent to the 0-simplex formed by that point.
|
Affine.Simplex.face_points'
theorem Affine.Simplex.face_points' :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor 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.orderEmbOfFin h)
This theorem states that for a given simplex `s` in the space of affine points `P` over a ring `k` with an additively commutative group `V` acting on it as a torsor, and a finite set `fs` of `n+1` elements (where `n` is a natural number), if the cardinality of `fs` is `m+1` for some natural number `m`, then the points of the face of the simplex defined by `fs` are given by composing the points of `s` with the function `fs.orderEmbOfFin`. Essentially, this means the points of the face of the simplex can be determined as a reordering of the points of the original simplex, as dictated by the function `fs.orderEmbOfFin h`, where `h` is the proven equality between the cardinality of `fs` and `m+1`.
More concisely: For a simplex `s` in the affine space over a ring `k` with a commutative group `V` acting as a torsor, and a finite set `fs` of `m+1` elements in `s` (where `m` is a natural number), the points of the face of `s` defined by `fs` are equal to the compositions of the points in `s` with the order embedding function `fs.orderEmbOfFin`.
|
Affine.Simplex.reindex_reindex_symm
theorem Affine.Simplex.reindex_reindex_symm :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {m n : ℕ} (s : Affine.Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)),
(s.reindex e).reindex e.symm = s
The theorem `Affine.Simplex.reindex_reindex_symm` states that for any Ring `k`, Additive Commutative Group `V`, Module `k` over `V`, and an Additive Torsor `V` over `P`, and given natural numbers `m` and `n`, a simplex `s` of `k` over `P` of dimension `m`, and an equivalence `e` from the set of `m+1` Fins to `n+1` Fins, reindexing the simplex `s` by this equivalence `e` and then reindexing again by the inverse of `e`, we get the original simplex `s`. In simpler terms, the process of reindexing a simplex twice, first with an equivalence and then with its inverse, results in the original simplex. This theorem is a formal statement about the invariance of the simplex under such transformations.
More concisely: For any Ring `k`, Additive Commutative Group `V`, Module `k` over `V`, Additive Torsor `V` over `P`, natural numbers `m` and `n`, simplex `s` of `k` over `P` of dimension `m`, and equivalence `e` from `m+1` Fins to `n+1` Fins, reindexing `s` by `e` and then by `e^(-1)` results in the original simplex `s`.
|
affineIndependent_of_ne_of_mem_of_not_mem_of_mem
theorem affineIndependent_of_ne_of_mem_of_not_mem_of_mem :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ p₃ : P},
p₁ ≠ p₃ → p₁ ∈ s → p₂ ∉ s → p₃ ∈ s → AffineIndependent k ![p₁, p₂, p₃]
This theorem states that for a given division ring `k`, an additive commutative group `V`, a module `V` over `k`, and an affine space `P` over `V`, along with an affine subspace `s` of `P` and three distinct points `p₁`, `p₂`, and `p₃` in `P`, if `p₁` and `p₃` are in `s` but `p₂` is not, then the points `p₁`, `p₂`, and `p₃` are affinely independent. In other words, these three points form a set where no nontrivial weighted subtractions (where the sum of weights is 0) are 0. This affinely independent condition is an important concept in affine geometry, similar to the notion of linear independence in linear algebra.
More concisely: Given a division ring `k`, an additive commutative group `V`, a `k`-module `V`, an affine space `P` over `V`, an affine subspace `s` of `P`, and three distinct points `p₁`, `p₂`, `p₃` in `P` with `p₁`, `p₃` in `s` and `p₂` not in `s`, these points are affinely independent.
|
AffineIndependent.range
theorem AffineIndependent.range :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P}, AffineIndependent k p → AffineIndependent k fun x => ↑x
This theorem states that if an indexed family of points is affinely independent, then the corresponding set of points is also affinely independent. Affine independence is defined in terms of weighted sums: a family of points is affinely independent if no nontrivial weighted sum of the points (where the sum of the weights is zero) equals zero. Here, "nontrivial" means that not all the weights are zero. In other words, if a linear combination of the points in the family (with the weights summing to zero) equals zero, then all the weights must be zero. The theorem asserts that this property is preserved when passing from an indexed family to its image set.
More concisely: If a family of points is affinely independent, then the set of their images under a function is also affinely independent.
|
affineIndependent_iff
theorem affineIndependent_iff :
∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_5}
{p : ι → V},
AffineIndependent k p ↔
∀ (s : Finset ι) (w : ι → k), s.sum w = 0 → (s.sum fun e => w e • p e) = 0 → ∀ e ∈ s, w e = 0
The theorem `affineIndependent_iff` is a characterization of affine independence in terms of linear combinations when viewing a module as an affine space modeled on itself. Specifically, it states that for any ring `k`, additively commutative group `V`, module over `k` and `V`, and any mapping `p` from an indexed set `ι` to `V`, the mapping `p` is affinely independent if and only if for any finite subset `s` of `ι` and any weighting function `w` from `ι` to `k`, if the sum of weights is zero and the weighted sum of the points `p e` (scaled by the weights `w e`) is zero, then all the weights for the elements in `s` are zero.
More concisely: A family of vectors in a module over a ring is affinely independent if and only if for any finite subset and any weighting function with zero total weight, the weighted sum of the vectors is zero implies all weights are zero.
|
AffineIndependent.subtype
theorem AffineIndependent.subtype :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
AffineIndependent k p → ∀ (s : Set ι), AffineIndependent k fun i => p ↑i
This theorem states that if a family of points is affinely independent, then any subfamily of this family, indexed by a subset of the index set, is also affinely independent. Here, affinely independent means that no nontrivial linear combination of the points (where the coefficients sum to zero) results in the zero vector. In other words, there is no linearly dependent subset among these points. The subfamily is formed by selecting points from the original family using a set of indices, and it also preserves the property of affine independence.
More concisely: If a set of points is affinely independent, then any subset of points selected from it using any index subset is also affinely independent.
|
AffineIndependent.of_set_of_injective
theorem AffineIndependent.of_set_of_injective :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
(AffineIndependent k fun x => ↑x) → Function.Injective p → AffineIndependent k p
The theorem `AffineIndependent.of_set_of_injective` states that for any type `k` that forms a ring, `V` that forms an additive commutative group, `P` that forms an additive torsor over `V`, and an indexed type `ι`, if you have an injective function `p` from `ι` to `P`, and the range of this function is an affinely independent set in the sense that no nontrivial weighted subtractions (where the sum of the weights is 0) are zero, then the function `p` itself is affinely independent. In other words, if an indexed family of points is injective and its range is affinely independent, then the indexed family itself is also affinely independent.
More concisely: If `p:` `ι` → `P` is an injective function from an indexed type `ι` to an additive commutative group `P` over a ring `k`, and the range `{p i | i ∈ ι}` is affinely independent in `P`, then `p` is an affinely independent family in `P`.
|
Affine.Simplex.reindex_range_points
theorem Affine.Simplex.reindex_range_points :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor 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
This theorem, named `Affine.Simplex.reindex_range_points`, states that for any affine simplex `s` of type `k` with points in `P` and of dimension `m`, and any bijection `e` from the set of `m + 1` natural numbers to the set of `n + 1` natural numbers, the range of the points of the reindexed simplex `(s.reindex e)` is the same as the range of the points of the original simplex `s`. In other words, reindexing a simplex doesn't change the set of its points. This remains true in the context of a ring `k`, an additive commutative group `V`, and a module `V` over `k`, where `V` is an additive torsor for `P`.
More concisely: For any affine simplex `s` of dimension `m` with points in a set `P`, and any bijection `e` from `{0, ..., m}` to `{0, ..., n}`, the reindexed simplex `(s.reindex e)` has the same point set as the original simplex `s`.
|
affineIndependent_of_ne
theorem affineIndependent_of_ne :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {p₁ p₂ : P}, p₁ ≠ p₂ → AffineIndependent k ![p₁, p₂]
The theorem `affineIndependent_of_ne` states that for any type `k` with a division ring structure, `V` being an additive commutative group, `P` with an `AddTorsor V P` structure such that `V` is a module over `k`, and given two distinct points `p₁` and `p₂` in `P`, these two points are affinely independent. Affine independence, in this context, means that there is no nontrivial linear combination of these points that sums to zero, where the coefficients of the linear combination also sum to zero.
More concisely: For any additive commutative group `V` made into a module over a division ring `k`, and any two distinct points `p₁` and `p₂` in an additive torsor `P` over `V`, `p₁` and `p₂` are affinely independent.
|
Affine.Simplex.reindex_trans
theorem Affine.Simplex.reindex_trans :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor 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₂₃
This theorem, named `Affine.Simplex.reindex_trans`, states that for any three natural numbers `n₁`, `n₂`, and `n₃`, and any two equivalences `e₁₂` and `e₂₃` between finite sets of size `n₁ + 1`, `n₂ + 1`, and `n₃ + 1` respectively, and any `n₁`-dimensional affine simplex `s`, reindexing the vertices of `s` by the composition of `e₁₂` and `e₂₃` is the same as first reindexing `s` by `e₁₂` and then reindexing the result by `e₂₃`. Here, the k is a Ring, V is an additive commutative group, and P is a module over k with a designated "zero" element, satisfying certain properties, and reindexing is a transformation acting on the vertices of an affine simplex.
More concisely: Given three natural numbers `n₁, n₂, n₃` and equivalences `e₁₂ : Finset.equiv (Finset.univ : Finset.{max n₁} -> Set) (Finset.univ : Finset.{max n₂} -> Set)` and `e₂₃ : Finset.equiv (Finset.univ : Finset.{max n₂} -> Set) (Finset.univ : Finset.{max n₃} -> Set)`, and an `n₁`-dimensional affine simplex `s` over a ring `k`, a commutative group `V`, and a module `P` over `k` with a designated "zero" element, the reindexing of `s` by `e₁₂ ∘ e₂₃` is equal to the reindexing of `s` by `e₁₂` followed by the reindexing of the result by `e₂₃`.
|
Affine.Simplex.face_centroid_eq_iff
theorem Affine.Simplex.face_centroid_eq_iff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : CharZero 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₂
This theorem states that over a division ring with characteristic zero, for a given simplex 's', the centroids of two of its faces (namely faces determined by finite sets 'fs₁' and 'fs₂') are equal if and only if those faces are defined by the exact same subset of points. Here, 'fs₁' and 'fs₂' are finite sets of points in the simplex, with cardinalities 'm₁ + 1' and 'm₂ + 1' respectively. The centroid of a face is computed as the 'Finset.centroid' with the 'Finset.univ' set of points of the face. In simpler terms, if two faces of the simplex have the exact same centroid, then they must be composed of the same points.
More concisely: In a division ring of characteristic zero, two simplices with equal centroid have identical point sets as their faces.
|
AffineMap.affineIndependent_iff
theorem AffineMap.affineIndependent_iff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [inst_4 : AddCommGroup V₂]
[inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {p : ι → P} (f : P →ᵃ[k] P₂),
Function.Injective ⇑f → (AffineIndependent k (⇑f ∘ p) ↔ AffineIndependent k p)
The theorem `AffineMap.affineIndependent_iff` states that for any ring `k`, additive commutative groups `V` and `V₂`, modules `V` and `V₂` over `k`, add-torsors `P` and `P₂` over `V` and `V₂` respectively, and any indexed family `p : ι → P`, if we have an injective affine map `f : P →ᵃ[k] P₂`, then the image of `p` under `f` (denoted `⇑f ∘ p`) is affinely independent if and only if `p` is affinely independent. Here, an indexed family `p` is said to be affinely independent if for every finite subset `s` of the indexing set `ι` and any weight function `w : ι → k` such that the sum of weights is zero and the weighted sum of vectors from `p` to the points in `s` is zero, then the weight assigned to each point in `s` by `w` is also zero.
More concisely: For any injective affine map between add-torsors over commutative additive groups and modules over a ring, if the preimage family is affinely independent, then the image family is affinely independent.
|
Affine.Simplex.reindex_symm_reindex
theorem Affine.Simplex.reindex_symm_reindex :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {m n : ℕ} (s : Affine.Simplex k P m) (e : Fin (n + 1) ≃ Fin (m + 1)),
(s.reindex e.symm).reindex e = s
The theorem `Affine.Simplex.reindex_symm_reindex` states that for any affine simplex `s` in a vector space `V` over a ring `k` with points `P`, and a given equivalence `e` between finite ordered sets `Fin (n + 1)` and `Fin (m + 1)`, if you first reindex the simplex `s` by the inverse of `e` and then reindex again by `e`, you will get back the original simplex `s`. In other words, the process of reindexing by an inverse and then the original equivalence leaves the simplex unchanged.
More concisely: For any affine simplex `s` in a vector space `V` over a ring `k`, and an equivalence `e` between `Fin (n + 1)` and `Fin (m + 1)`, reindexing `s` by `e` and then by `e^−1` is equivalent to leaving `s` unchanged.
|
Affine.Simplex.face_centroid_eq_centroid
theorem Affine.Simplex.face_centroid_eq_centroid :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor 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
This theorem states that for a given simplex `s` in a space with scalars `k`, vector type `V`, and point type `P` (where `k` is a division ring, `V` is an additive commutative group, and `P` is an affine torsor over `V`), and for a given subset `fs` of the finite type `Fin (n + 1)`, if the cardinality of `fs` is `m + 1`, then the centroid of the face of the simplex determined by `fs` is the same as the centroid of the subset `fs` of the points of the simplex `s`. In other words, the centroid of a face of a simplex is the same as the centroid of the set of points that define that face.
More concisely: The centroid of a face of a simplex in a vector space with scalars `k`, vector type `V`, and point type `P` is equal to the centroid of the subset of points of the simplex defining that face.
|
affineIndependent_of_subsingleton
theorem affineIndependent_of_subsingleton :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : Subsingleton ι] (p : ι → P), AffineIndependent k p
The theorem `affineIndependent_of_subsingleton` establishes that, for any type `k` (which is a ring), and given types `V` and `P` (such that `V` is an additive commutative group, `P` is an additively translatable space with `V` as the space of translations, and `V` is a `k`-module), if the index set `ι` is a subsingleton (i.e., has at most one element), then any function from `ι` to `P` is affinely independent. In other words, if a family of points in `P` has at most one point, it is affinely independent, meaning that no nontrivial weighted subtraction of the points (where the sum of weights is 0) equals 0.
More concisely: Given a ring `k`, an additive commutative group `V` (a `k`-module), and an additively translatable space `P` over `V`, if `ι` is a subsingleton, then any function from `ι` to `P` consists of affinely independent points.
|
Affine.Simplex.reindex_refl
theorem Affine.Simplex.reindex_refl :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n), s.reindex (Equiv.refl (Fin (n + 1))) = s
The theorem `Affine.Simplex.reindex_refl` states that for any simplex `s` of type `Affine.Simplex` in a module over a ring, reindexing the simplex using the identity equivalence (`Equiv.refl`), which maps each type to itself, results in the original simplex. This holds true regardless of the number `n` of elements in the simplex, and for any ring `k`, additive commutative group `V`, and additive torsor `P`.
More concisely: For any simplex `s` of type `Affine.Simplex` in a module over a ring, the reindexing of `s` using the identity equivalence equals `s`.
|
Affine.Simplex.ext
theorem Affine.Simplex.ext :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {n : ℕ} {s1 s2 : Affine.Simplex k P n},
(∀ (i : Fin (n + 1)), s1.points i = s2.points i) → s1 = s2
This theorem states that, given two simplices `s1` and `s2`, each with `n + 1` points, which exist within a module with a ring of type `k`, a commutative group of type `V`, and an additive torsor of type `P`, if every corresponding point of `s1` and `s2` are equivalent (i.e., the `i`-th point of `s1` is equal to the `i`-th point of `s2` for all `i`), then the two simplices `s1` and `s2` are equal.
More concisely: Given two simplices `s1` and `s2` with `n + 1` points in a module over a ring `k`, with a commutative group `V` and an additive torsor `P`, if each point of `s1` is equivalent to the corresponding point of `s2`, then `s1` and `s2` are equal.
|
Affine.Simplex.centroid_eq_iff
theorem Affine.Simplex.centroid_eq_iff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : CharZero k] {n : ℕ} (s : Affine.Simplex k P n)
{fs₁ fs₂ : Finset (Fin (n + 1))} {m₁ m₂ : ℕ},
fs₁.card = m₁ + 1 →
fs₂.card = m₂ + 1 → (Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂)
This theorem states that, given a division ring with characteristic zero and a simplex, the centroids calculated from two subsets of the simplex's points are equivalent if and only if those subsets of points are the same. For the subsets of points, their cardinalities must be one more than some natural numbers (m₁ and m₂ respectively) for the equivalence to hold. This theorem applies to the scenario where the division ring is used as the scalar field for vector space operations, and the AddTorsor structure allows for the addition of a vector from the vector space to a point in the affine space.
More concisely: Given a division ring of characteristic zero and a simplex, the centroids of subsets of its points with cardinality one more than some natural numbers are equal if and only if the subsets are equal.
|
Affine.Simplex.face_points
theorem Affine.Simplex.face_points :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor 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.orderEmbOfFin h) i)
This theorem states that for a given simplex `s` defined in an affine space, the points of any face of the simplex (represented by a subset `fs`) are determined by `mono_of_fin`. In other words, for any face `fs` of the simplex `s` with cardinality `m+1` and for any index `i`, the `i`-th point of this face is the same as the `((fs.orderEmbOfFin h) i)`-th point of the original simplex `s`. Here, `orderEmbOfFin` is a function that computes an increasing bijection from a finite subset of a finite type to `fin n` for some `n`.
More concisely: For any simplex `s` in an affine space and face `fs` of `s` with `m+1` points, the `i`-th point of `fs` is equal to the `((fs.orderEmbOfFin h) i)`-th point of `s`, where `h` is the inclusion map of `fs` into `s`.
|
AffineIndependent.mono
theorem AffineIndependent.mono :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s t : Set P},
(AffineIndependent k fun x => ↑x) → s ⊆ t → AffineIndependent k fun x => ↑x
The theorem `AffineIndependent.mono` states that if a set of points is affinely independent, then any subset of that set is also affinely independent. Here, affine independence is defined such that no nontrivial weighted subtractions (where the sum of weights is zero) are zero. The terms in the theorem are from the field of vector spaces and affine geometry. In this context, a set of points is considered to be a set of vectors in a vector space. The theorem is parameterized over a generic ring `k`, a group `V` under addition, and a module `P` over `k`. The theorem also assumes the existence of an operation `AddTorsor` that enables subtraction of vectors and translation by vectors.
More concisely: If a subset of affinely independent vectors in a module over a ring forms a linearly dependent set, then it contains a nontrivial linear dependence relation that can be extended to involve only vectors from the original affinely independent set.
|
AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan
theorem AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : Nontrivial k] {p : ι → P},
AffineIndependent k p →
∀ {s1 s2 : Set ι} {p0 : P}, p0 ∈ affineSpan k (p '' s1) → p0 ∈ affineSpan k (p '' s2) → ∃ i, i ∈ s1 ∩ s2
The theorem `AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan` states that given a family of points that are affinely independent (i.e., no non-trivial weighted subtractions, where the sum of weights is 0, are 0), and two subsets of these points' indices which have a common point in their respective affine spans, then there exists an index that is common to both subsets. This property holds when the underlying algebraic structure is a nontrivial ring. In other words, if two different sets of points, defined by their indices, in an affinely independent family share a point in their smallest containing affine subspaces, then these sets of indices must have a common element.
More concisely: Given a finite family of points in a nontrivial affine space over a ring, if two subsets of indices have a common point in their affine spans and the points are affinely independent, then there exists a common index in the two subsets.
|
AffineIndependent.affineIndependent_of_not_mem_span
theorem AffineIndependent.affineIndependent_of_not_mem_span :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P} {i : ι},
(AffineIndependent k fun x => p ↑x) → p i ∉ affineSpan k (p '' {x | x ≠ i}) → AffineIndependent k p
This theorem states that given a family of points indexed by `ι` (denoted by `p : ι → P`) in an affine space over a division ring `k`, if all points except one (say `i`) are affinely independent, and the point `i` does not lie in the affine span of the rest of the family, then the whole family `p` is affinely independent. Here, affine independence means that no nontrivial weighted sum of the points (where weights sum to zero) is the zero vector, and affine span of a set of points is the smallest affine subspace containing those points.
More concisely: If a family of points in an affine space over a division ring is almost affinely independent and none of them is in the affine span of the others, then the family is affinely independent.
|
Affine.Simplex.ext_iff
theorem Affine.Simplex.ext_iff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {n : ℕ} (s1 s2 : Affine.Simplex k P n),
s1 = s2 ↔ ∀ (i : Fin (n + 1)), s1.points i = s2.points i
This theorem states that in the context of affine simplices over a ring with module and additive torsor structure, two simplices are equal if and only if their corresponding points are the same for all indices within the dimension of the simplices plus one. An affine simplex here can be understood as a generalization of a triangle or a tetrahedron to arbitrary dimensions, and the points constitute its vertices.
More concisely: In the context of affine simplices over a ring with module and additive torsor structure, two simplices are equal if and only if their corresponding vertices agree up to dimension.
|
affineIndependent_of_ne_of_mem_of_mem_of_not_mem
theorem affineIndependent_of_ne_of_mem_of_mem_of_not_mem :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ p₃ : P},
p₁ ≠ p₂ → p₁ ∈ s → p₂ ∈ s → p₃ ∉ s → AffineIndependent k ![p₁, p₂, p₃]
This theorem states that given three distinct points `p₁`, `p₂`, and `p₃`, if `p₁` and `p₂` are both in an `AffineSubspace s` but `p₃` is not, then the three points are affinely independent. Affine independence here means that no nontrivial linear combination of these points (where the coefficients sum to zero) results in the zero vector. This condition ensures that no point in the set can be expressed as a linear combination of the others, which is a crucial property in many geometric and algebraic operations.
More concisely: If three distinct points `p₁`, `p₂`, and `p₃` lie in an affine subspace `s` but `p₃` is not, then they are affinely independent, meaning no nontrivial linear combination of `p₁`, `p₂`, and `p₃` equals the zero vector.
|
affineIndependent_def
theorem affineIndependent_def :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P),
AffineIndependent k p ↔
∀ (s : Finset ι) (w : ι → k), (s.sum fun i => w i) = 0 → (s.weightedVSub p) w = 0 → ∀ i ∈ s, w i = 0
The theorem `affineIndependent_def` states that for a given indexed family `p` (a function mapping from some index set `ι` to points `P`), the family is affinely independent over some field `k` with respect to some vectors `V` (which forms a module over `k` and an additive torsor with `P`) if and only if for any finite subset `s` of the index set and any weight function `w` mapping from the index set to `k`, if the sum of weights in `s` is zero and the weighted subtraction of `p` over the weights `w` in `s` is also zero, then all the weights of the elements in `s` must be zero. This captures the geometric intuition that no point in the indexed family can be written as a nontrivial affine combination of other points in the family.
More concisely: The family `p` indexed over `ι` is affinely independent over the field `k` with respect to the module `V` if and only if for any finite subset `s` of `ι` and any weight function `w` such that the sum of `w` over `s` is zero implies that all the weights `w(i)` for `i` in `s` are zero.
|
affineCombination_mem_affineSpan_pair
theorem affineCombination_mem_affineSpan_pair :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
AffineIndependent k p →
∀ {w w₁ w₂ : ι → k} {s : Finset ι},
(s.sum fun i => w i) = 1 →
(s.sum fun i => w₁ i) = 1 →
(s.sum fun i => w₂ i) = 1 →
((Finset.affineCombination k s p) w ∈
affineSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂} ↔
∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i)
This theorem states that given an affinely independent family of points, an affine combination of these points lies within the affine span of two other affine combinations of these points if and only if the weights used for this affine combination can be expressed as the weights for one of the combinations plus a multiple of the difference between the weights of the two combinations. This is under the condition that the sum of weights for each of the three affine combinations is 1.
More concisely: Given affinely independent points, an affine combination of these points lies in the affine hull spanned by two other combinations if and only if the difference of their weights is a scalar multiple of the weights for the first combination.
|
AffineIndependent.affineSpan_disjoint_of_disjoint
theorem AffineIndependent.affineSpan_disjoint_of_disjoint :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : Nontrivial k] {p : ι → P},
AffineIndependent k p →
∀ {s1 s2 : Set ι}, Disjoint s1 s2 → Disjoint ↑(affineSpan k (p '' s1)) ↑(affineSpan k (p '' s2))
This theorem states that for a given family of affinely independent points, if two subsets of these points are disjoint (in the sense that they don't share common elements), then their corresponding affine spans are also disjoint, provided that the underlying ring is nontrivial. In other words, if you take two groups of points from an affinely independent set, such that no point is in both groups, the smallest affine subspaces containing these groups respectively will have no overlap, assuming that the coefficients used to generate these subspaces come from a nontrivial ring.
More concisely: Given a set of affinely independent points in a nontrivial ring, two disjoint subsets of these points have disjoint affine spans.
|
Affine.Simplex.range_face_points
theorem Affine.Simplex.range_face_points :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor 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
This theorem states that for any affine simplex `s` of a certain dimension `n`, and a face `fs` of the simplex with `m + 1` vertices, the set of points that constitute this face, denoted `(s.face h).points`, is precisely the image of the set of vertices `fs` under the point mapping of the simplex `s`. This indicates that any point on the face can be uniquely determined by the simplex's point mapping applied to one of the vertices of the face, and vice-versa, every vertex of the face maps to a unique point on the face via the simplex's point mapping. The underlying structure assumes a ring `k`, an additively commutative group `V`, and `V` is a module over the ring `k`. Additionally, `V` acts on `P` via an additive torsor structure.
More concisely: For any affine simplex `s` of dimension `n` and its face `fs` with `m + 1` vertices, the points of the face `(s.face h).points` are exactly the images of the vertices `fs` under `s`'s point mapping.
|
affineIndependent_iff_indicator_eq_of_affineCombination_eq
theorem affineIndependent_iff_indicator_eq_of_affineCombination_eq :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P),
AffineIndependent k p ↔
∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
(s1.sum fun i => w1 i) = 1 →
(s2.sum fun i => w2 i) = 1 →
(Finset.affineCombination k s1 p) w1 = (Finset.affineCombination k s2 p) w2 →
(↑s1).indicator w1 = (↑s2).indicator w2
This theorem states that a family of points is affinely independent if and only if, for any two sets of affine combinations (where the sum of weights is 1) that evaluate to the same point, the indicator functions of the sets with respect to the weights are equal. In other words, if two weighted sums of the points give the same result, then the weights assigned to each point in the two sums must be the same. In this context, the function 'AffineIndependent' is defined on a family of points where no nontrivial weighted subtraction (with total weight summing to zero) equals zero. The 'indicator function' is a function defined on the set that is equal to the corresponding weight if the point is in the set, and zero otherwise.
More concisely: A family of points is affinely independent if and only if the indicator functions of any two sets of affine combinations that map to the same point have identical weights for each point in the family.
|
affineIndependent_of_ne_of_not_mem_of_mem_of_mem
theorem affineIndependent_of_ne_of_not_mem_of_mem_of_mem :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ p₃ : P},
p₂ ≠ p₃ → p₁ ∉ s → p₂ ∈ s → p₃ ∈ s → AffineIndependent k ![p₁, p₂, p₃]
The theorem `affineIndependent_of_ne_of_not_mem_of_mem_of_mem` states that for any Division Ring `k`, Additive Commutative Group `V`, Additive Torsor `P`, and Affine Subspace `s` of `k` and `P`, given three points `p₁`, `p₂`, and `p₃` such that `p₂` and `p₃` are distinct and lie in `s` and `p₁` does not lie in `s`, then the three points `p₁`, `p₂`, and `p₃` are affinely independent. Affine independence in this context means that no nontrivial linear combination of these points (where the coefficients sum to zero) yields the zero vector.
More concisely: Given a division ring `k`, an additive commutative group `V`, an additive torsor `P` over `V`, and an affine subspace `s` of `k` and `P`, if `p₁` is not in `s` and `p₂` and `p₃` are distinct points in `s`, then `p₁`, `p₂`, and `p₃` are affinely independent in `k` and `P`.
|
AffineIndependent.map'
theorem AffineIndependent.map' :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [inst_4 : AddCommGroup V₂]
[inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {p : ι → P},
AffineIndependent k p → ∀ (f : P →ᵃ[k] P₂), Function.Injective ⇑f → AffineIndependent k (⇑f ∘ p)
The theorem `AffineIndependent.map'` states that for any indexed family of points in an affine space, if it is affinely independent, then its image under an injective affine transformation will also be affinely independent. In more detail, given a set of points in an affine space over a ring `k` indexed by `ι` and satisfying the condition of affine independence, when these points are mapped to a new affine space (also over `k`) by a function `f` that preserves affine structures and is injective (i.e. distinct points are always mapped to distinct points), the resulting set of points in the new affine space retains the property of affine independence.
More concisely: If `{x_i : V | i ∈ ι}` is an affinely independent family of points in an affine space `V` over a ring `k`, and `f : V → W` is an injective function between affine spaces `V` and `W` over `k`, then `{f(x_i) : W}` is an affinely independent family of points in `W`.
|
affineIndependent_set_iff_linearIndependent_vsub
theorem affineIndependent_set_iff_linearIndependent_vsub :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set P} {p₁ : P},
p₁ ∈ s →
((AffineIndependent k fun p => ↑p) ↔ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v)
The theorem `affineIndependent_set_iff_linearIndependent_vsub` states that a set is affinely independent if and only if the vectors obtained by subtracting a base point from each point in the set are linearly independent. Here, the base point is an element of the set. This theorem establishes the equivalence between affine independence and linear independence of set differences. The type `k` is the field over which vectors are considered, `V` is the type of vectors, and `P` is the type of points. The set `s` is a set of points and `p₁` is a point in `s`. The affine independence is defined over a function that maps each point in `s` to itself, and the linear independence is over a function mapping each of the vectors resulting from subtracting `p₁` (omitting `p₁` itself) to themselves.
More concisely: A set of vectors obtained by subtracting a base point from a set of affine-independent points forms a linearly independent set over a field.
|
AffineEquiv.affineIndependent_set_of_eq_iff
theorem AffineEquiv.affineIndependent_set_of_eq_iff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {V₂ : Type u_5} {P₂ : Type u_6} [inst_4 : AddCommGroup V₂] [inst_5 : Module k V₂]
[inst_6 : AddTorsor V₂ P₂] {s : Set P} (e : P ≃ᵃ[k] P₂),
AffineIndependent k Subtype.val ↔ AffineIndependent k Subtype.val
This theorem declares that affine equivalences preserve the affine independence of subsets. Here, the setting is a given ring `k` and a pair of torsors `V` and `V₂` over `k` which define two affine spaces `P` and `P₂` respectively. The main claim is that given an affine equivalence `e` from P to P₂ and a set `s` of points in `P`, if we consider the subset of points in `P` which are affinely independent (where the independence refers to the base type points represented by `Subtype.val`), this property of affine independence is maintained under the given equivalence `e`. Conversely, every affinely independent set in `P₂` corresponds to an affinely independent set in `P` under the inverse of `e`. Hence, the affine equivalence `e` provides a bijection between affinely independent sets in `P` and `P₂`.
More concisely: Given an affine equivalence between two affine spaces, the sets of affine-independent points in the corresponding affine spaces are in bijection.
|
AffineIndependent.units_lineMap
theorem AffineIndependent.units_lineMap :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
AffineIndependent k p →
∀ (j : ι) (w : ι → kˣ), AffineIndependent k fun i => (AffineMap.lineMap (p j) (p i)) ↑(w i)
The theorem `AffineIndependent.units_lineMap` states that for any ring `k`, additively commutative group `V`, module `k V`, additively translatable space `V P`, and an indexed family of points `p` in `P` that is affine independent, if we pick a single member `j` from the indexed family and move all other members along the line joining them to `j` by a factor of `w`, the resulting family of points remains affine independent. This theorem is an affine version of `LinearIndependent.units_smul`. This affine transformation is achieved using the `AffineMap.lineMap` function. This theorem ensures the preservation of affine independence under such transformations.
More concisely: Given a ring `k`, an additively commutative group `V`, a module `k V`, an additively translatable space `V P`, an affine independent family `p` in `P`, and `w` in `k`, the family `{p_i + w * (p_j - p_i) | i ≠ j}` is affine independent.
|
weightedVSub_mem_vectorSpan_pair
theorem weightedVSub_mem_vectorSpan_pair :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
AffineIndependent k p →
∀ {w w₁ w₂ : ι → k} {s : Finset ι},
(s.sum fun i => w i) = 0 →
(s.sum fun i => w₁ i) = 1 →
(s.sum fun i => w₂ i) = 1 →
((s.weightedVSub p) w ∈
vectorSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂} ↔
∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ i))
This theorem states that, given an affinely independent family of points, a weighted subtraction, where the sum of weights is zero, lies in the vector span of two points given as affine combinations if and only if the weights of this subtraction can be written as a multiple of the difference between the weights of the two points. More formally, for weights `w`, `w₁`, and `w₂` and a finite set `s`, if the sum over `s` of `w` is zero and the sums over `s` of `w₁` and `w₂` are both one, then the weighted subtraction of `p` with respect to `w` is in the vector span of the affine combinations of `s` and `p` with respect to `w₁` and `w₂` if and only if there exists a scalar `r` such that for all `i` in `s`, `w i` equals `r` times the difference between `w₁ i` and `w₂ i`. This theorem connects the concepts of affine independence, weighted subtraction, vector span, and affine combination.
More concisely: Given affinely independent points and weights with zero sum and unit sums for each point, a weighted subtraction lies in the vector span of two points if and only if the weights represent a scalar multiple of the difference between the weights of the two points.
|
AffineEquiv.affineIndependent_iff
theorem AffineEquiv.affineIndependent_iff :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [inst_4 : AddCommGroup V₂]
[inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {p : ι → P} (e : P ≃ᵃ[k] P₂),
AffineIndependent k (⇑e ∘ p) ↔ AffineIndependent k p
The theorem `AffineEquiv.affineIndependent_iff` states that affine equivalences preserve the affine independence of families of points. More precisely, given a type `k` equipped with a ring structure, types `V` and `P` with `V` an additive commutative group and `P` an affine space over `V`, an indexing type `ι`, and a similar structure for `V₂` and `P₂`, if `p` is a function from `ι` to `P` and `e` is an affine equivalence from `P` to `P₂`, then the transformed function `e ∘ p` is affinely independent if and only if the original function `p` is affinely independent. Affine independence is defined as: for any finite subset `s` of `ι`, and any weighting function `w` from `ι` to `k` that sums to zero, if the weighted sum of vectors from the function `p` to the points subtracted by the function `p` is zero, then the weight of each point in `s` must be zero.
More concisely: Given affine spaces `P` and `P₂` over an additive commutative group `V` with ring structure `k`, an affine equivalence `e` between them, a function `p` from an indexing type `ι` to `P`, and any finite subset `s` of `ι` and weighting function `w` from `ι` to `k` summing to zero, `p` is affinely independent if and only if `e ∘ p` is affinely independent in `P₂`.
|
Affine.Simplex.centroid_eq_of_range_eq
theorem Affine.Simplex.centroid_eq_of_range_eq :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {n : ℕ} {s₁ s₂ : Affine.Simplex k P n},
Set.range s₁.points = Set.range s₂.points →
Finset.centroid k Finset.univ s₁.points = Finset.centroid k Finset.univ s₂.points
The theorem `Affine.Simplex.centroid_eq_of_range_eq` states that for any division ring `k`, additively commutative group `V`, and an affine torsor `P` over `V`, if two `n`-dimensional simplices `s₁` and `s₂` have the same set of points, then their centroids are also the same. In other words, if the range of the point mapping function of the first simplex is equal to the range of the point mapping function of the second simplex, then the centroids of these two simplices, calculated as the affine combination of points using the universal finite set of their types (implied from the `Fintype` of their types), are also equal.
More concisely: If two `n`-dimensional simplices over an additively commutative group `V` in a division ring `k` have the same set of points, then their centroids are equal.
|
AffineIndependent.comp_embedding
theorem AffineIndependent.comp_embedding :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} {ι2 : Type u_5} (f : ι2 ↪ ι) {p : ι → P},
AffineIndependent k p → AffineIndependent k (p ∘ ⇑f)
The theorem `AffineIndependent.comp_embedding` states that, for any given set of types `k`, `V`, `P`, `ι`, and `ι2` where `k` is a ring, `V` is an additive commutative group, `V` is a module over `k`, and `P` is an affine torsor over `V`; if we have a family `p` indexed by `ι` that is affinely independent, and an embedding `f` from `ι2` into `ι`, then the subfamily resulting from the composition of `p` with `f` (i.e., `p ∘ ⇑f`) is also affinely independent. In other words, any subfamily of an affinely independent family, derived via an embedding into the index type, preserves the property of affine independence.
More concisely: Given a ring `k`, an additive commutative group `V` that is a `k`-module, an affine torsor `P` over `V`, an affinely independent family `p:` `ι` → `P`, and an embedding `f:` `ι2` → `ι`, the subfamily `p ∘ ⇑f` of `P` indexed by `ι2` is also affinely independent.
|
exists_subset_affineIndependent_affineSpan_eq_top
theorem exists_subset_affineIndependent_affineSpan_eq_top :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] {s : Set P},
(AffineIndependent k fun p => ↑p) → ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
The theorem `exists_subset_affineIndependent_affineSpan_eq_top` states that for any division ring `k`, additively commutative group `V`, module `k V`, and addition torsor `V P`, given any set `s` of points `P`, if the set is affinely independent (i.e., no nontrivial weighted subtractions, where the sum of weights is 0, are 0), then there exists a superset `t` of `s` that is also affinely independent and that spans the whole space (i.e., the affine span of `t` is the entire space).
More concisely: For any division ring `k`, additively commutative group `V`, module `k V`, and addition torsor `V P`, if `s` is a set of affinely independent points in `V`, then there exists a larger affinely independent set `t` contained in `s` whose affine span equals the whole space `V`.
|
linearIndependent_set_iff_affineIndependent_vadd_union_singleton
theorem linearIndependent_set_iff_affineIndependent_vadd_union_singleton :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s : Set V},
(∀ v ∈ s, v ≠ 0) → ∀ (p₁ : P), (LinearIndependent k fun (v : ↑s) => ↑v) ↔ AffineIndependent k fun p => ↑p
This theorem states that for any ring `k`, an additive commutative group `V`, a module `k V`, and an additive torsor `V P`, along with a set `s` of vectors in `V` such that all vectors in `s` are nonzero, and any point `p₁` in `P`, the set `s` of vectors is linearly independent over `k` if and only if the set consisting of the vectors in `s` each added to `p₁`, along with `p₁` itself, is affinely independent over `k`. In other words, a set of nonzero vectors can only be linearly independent if adding a specific point to each of these vectors and also considering the point itself forms a set that is affinely independent.
More concisely: For any additive torsor `V P` over a ring `k`, a set `s` of nonzero vectors in the module `k V` is linearly independent if and only if the set of vectors in `s` together with the point `p₁` in `P` is affinely independent.
|
affineIndependent_iff_linearIndependent_vsub
theorem affineIndependent_iff_linearIndependent_vsub :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) (i1 : ι),
AffineIndependent k p ↔ LinearIndependent k fun i => p ↑i -ᵥ p i1
The theorem `affineIndependent_iff_linearIndependent_vsub` states that for any type `k` with a ring structure, and types `V` and `P` such that `V` is an additive commutative group and is a module over `k`, and `P` is an additive torsor over `V`, given a function `p` from type `ι` to `P` and an element `i1` of type `ι`, a family of points `p` in `P` indexed by `ι` is affinely independent if and only if the family of vectors obtained by subtracting the point `p i1` from each point `p i` (for `i` in `ι`) is linearly independent over `k`. In other words, no nontrivial linear combination of the differences between the points in the family and a fixed base point equals zero if and only if no nontrivial weighted subtraction of the points in the family (where the sum of the weights is zero) equals zero.
More concisely: Given a ring `k`, an additive commutative group and `k`-module `V`, an additive torsor `P` over `V`, and a family `p` of points in `P`, the family is affinely independent if and only if the family of vectors obtained by subtracting a fixed point from each point in the family is linearly independent over `k`.
|
AffineIndependent.injective
theorem AffineIndependent.injective :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : Nontrivial k] {p : ι → P},
AffineIndependent k p → Function.Injective p
The theorem states that, given a nontrivial ring 'k', an additive commutative group 'V', a module 'V' over the ring 'k', a torsor 'P' over the group 'V', and a mapping 'p' from an arbitrary type 'ι' to 'P', if the family indexed by 'ι' is affinely independent under 'p', then 'p' is an injective function. In simpler terms, for an affinely independent family under a nontrivial ring, no two distinct elements in the domain of 'p' can map to the same value in its codomain. This injectivity ensures uniqueness in the representation of points in the affinely independent set.
More concisely: Given a nontrivial ring 'k', a module 'V' over 'k', a torsor 'P' over an additive commutative group 'V', and a mapping 'p' from an arbitrary type 'ι' to 'P', if the family indexed by 'ι' is affinely independent under 'p', then 'p' is an injective function.
|
Affine.Simplex.mkOfPoint_points
theorem Affine.Simplex.mkOfPoint_points :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] (p : P) (i : Fin 1), (Affine.Simplex.mkOfPoint k p).points i = p
The theorem `Affine.Simplex.mkOfPoint_points` states that for any type `k`, and types `V` and `P` with `k` being a ring, `V` being an additive commutative group, `V` being a module over `k`, and `V` being an additive torsor over `P`, given a point `p` in `P` and an index `i` in `Fin 1` (i.e., a 0 or 1), the point at index `i` in the 0-simplex created from `p` using the `Affine.Simplex.mkOfPoint` function is `p`. In other words, the point used to construct the 0-simplex is the only point in the simplex.
More concisely: For any ring `k`, additive commutative group `V` that is a `k`-module and additive torsor over `P`, and point `p` in `P`, the point at index 0 in the 0-simplex created from `p` using `Affine.Simplex.mkOfPoint` equals `p`.
|
AffineIndependent.of_comp
theorem AffineIndependent.of_comp :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {ι : Type u_4} {V₂ : Type u_5} {P₂ : Type u_6} [inst_4 : AddCommGroup V₂]
[inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {p : ι → P} (f : P →ᵃ[k] P₂),
AffineIndependent k (⇑f ∘ p) → AffineIndependent k p
The theorem `AffineIndependent.of_comp` states that for any ring `k`, additively commutative groups `V` and `V₂`, modules `V` and `V₂` over `k`, torsors `V` and `V₂` for `P` and `P₂`, and any mapping `p` from an index set `ι` to `P`, if a family of points in an affine space `P₂` is affine-independent under an affine transformation `f` from `P` to `P₂`, then the original family of points in `P` is also affine-independent. In other words, the property of affine-independence is preserved under affine transformations.
More concisely: Given rings `k`, additively commutative groups/modules `V` and `V₂`, torsors `V` and `V₂` for `P` and `P₂`, and a mapping `p` from an index set `ι` to `P`, if a family of points in `P₂` is affine-independent under an affine transformation `f` from `P` to `P₂`, then the family of `f⁻¹(points)` in `P` is also affine-independent.
|