finrank_vectorSpan_range_le
theorem finrank_vectorSpan_range_le :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] (p : ι → P) {n : ℕ},
Fintype.card ι = n + 1 → FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) ≤ n
This theorem states that given a division ring `k`, an additive commutative group `V`, a 'torsor' or 'space' `P` under `V`, a finitely-typed indexing set `ι`, and a function `p` that maps from `ι` to `P`, if the cardinality of `ι` is `(n + 1)`, then the rank (or dimension) of the subspace spanned by the vectors formed from the differences of the points indexed by `ι` (denoted as `vectorSpan`) is less than or equal to `n`. In other words, this theorem is saying that the 'space' spanned by the differences of `n + 1` points has a dimension of at most `n`.
More concisely: Given a division ring `k`, an additive commutative group `V`, a torsor `P` under `V`, a finitely-typed indexing set `ι` with cardinality `n+1`, the rank of the subspace spanned by the differences of the corresponding points in `P` is less than or equal to `n`.
|
Coplanar.finiteDimensional_vectorSpan
theorem Coplanar.finiteDimensional_vectorSpan :
∀ {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},
Coplanar k s → FiniteDimensional k ↥(vectorSpan k s)
This theorem states that the vector span of any set of coplanar points in a vector space is finite-dimensional. Here, a set of points is considered coplanar if the dimension of their vector span is at most two. The vector span is the submodule comprising all differences between points in the set. The theorem then asserts that if this set of points is coplanar, then the vector space spanned by these differences is finite-dimensional. This means it has a finite basis, and therefore, the number of vectors needed to describe any point in the span is finite.
More concisely: The vector span of any set of coplanar points in a vector space is a finite-dimensional subspace.
|
Coplanar.finiteDimensional_direction_affineSpan
theorem Coplanar.finiteDimensional_direction_affineSpan :
∀ {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},
Coplanar k s → FiniteDimensional k ↥(affineSpan k s).direction
This theorem states that for any set of points 's' in an affine space over a division ring 'k' with an associated vector space 'V' and a set of points 'P', if these points are coplanar, then the direction of the affine span of these points is a finite-dimensional vector space. In other words, if a set of points lies on the same plane, the set of vectors that can be formed by considering every pair of points among these coplanar points is a finite-dimensional vector space.
More concisely: If a finite set of points in an affine space over a division ring is coplanar, then the vector space spanned by the pairs of points is finite-dimensional.
|
AffineIndependent.vectorSpan_eq_of_le_of_card_eq_finrank_add_one
theorem AffineIndependent.vectorSpan_eq_of_le_of_card_eq_finrank_add_one :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] {p : ι → P},
AffineIndependent k p →
∀ {sm : Submodule k V} [inst_5 : FiniteDimensional k ↥sm],
vectorSpan k (Set.range p) ≤ sm →
Fintype.card ι = FiniteDimensional.finrank k ↥sm + 1 → vectorSpan k (Set.range p) = sm
This theorem states that if we have a finite affinely independent family in a vector space, and the `vectorSpan` (submodule created by taking all possible differences of this set of points) of this family is contained in a submodule whose dimension is one less than the cardinality (number of unique elements) of the family, then the `vectorSpan` of the family is equal to this submodule. This theorem holds for any type of field, module, affine torsor, and indexing set.
More concisely: If a finite subset of a vector space has affine independence and the span of this subset has dimension one less than its cardinality, then the span of the subset equals the submodule containing it.
|
Collinear.mem_affineSpan_of_mem_of_ne
theorem Collinear.mem_affineSpan_of_mem_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] {s : Set P},
Collinear k s → ∀ {p₁ p₂ p₃ : P}, p₁ ∈ s → p₂ ∈ s → p₃ ∈ s → p₁ ≠ p₂ → p₃ ∈ affineSpan k {p₁, p₂}
This theorem states that for a collinear set of points (a set of points all lying on the same straight line) in an affine space over a division ring, if a point is a member of this set and is distinct from two other points in the set, then this point is contained within the affine span of those two other points. In other words, in a collinear set, any point can be expressed as a linear combination of any two other distinct points from the set.
More concisely: In an affine space over a division ring, any distinct collinear points determine a line through them, and any other collinear point can be expressed as a linear combination of those two.
|
finrank_vectorSpan_le_iff_not_affineIndependent
theorem finrank_vectorSpan_le_iff_not_affineIndependent :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] (p : ι → P) {n : ℕ},
Fintype.card ι = n + 2 →
(FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) ≤ n ↔ ¬AffineIndependent k p)
The theorem `finrank_vectorSpan_le_iff_not_affineIndependent` states that for a given division ring `k`, additive commutative groups `V` and `P`, a type `ι`, a module of `k` and `V`, an additive torsor of `V` and `P`, a function `p` from `ι` to `P`, and a natural number `n`, if the size of the set `ι` is `n + 2`, then the dimension of the `vectorSpan` created from the set of points given by function `p` is less than or equal to `n` if and only if the points are not affinely independent. Affine independence here is defined as the property that no nontrivial weighted subtractions (where the sum of weights is 0) are zero.
More concisely: For a division ring `k`, additive commutative groups `V` and `P`, a type `ι` of size `n + 2`, an additive torsor of `V` and `P`, a function `p` from `ι` to `P`, and natural number `n`, the dimension of the `vectorSpan` of points given by `p` is less than or equal to `n` if and only if these points are not affine independent, meaning no nontrivial weighted subtractions of these points sum to zero.
|
collinear_insert_iff_of_mem_affineSpan
theorem collinear_insert_iff_of_mem_affineSpan :
∀ {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} {p : P},
p ∈ affineSpan k s → (Collinear k (insert p s) ↔ Collinear k s)
This theorem states that for any division ring `k`, additive commutative group `V`, and add-torsor `P`, if `p` is a point in the affine span of a set `s`, then the property of `s` being collinear (i.e., all its points lie on a single line, or more formally, the `vectorSpan` of the set has a dimension at most `1`) remains unchanged even if `p` is added to `s`. In other words, inserting a point `p` that is already in the affine span of a set `s` does not affect the collinearity of `s`.
More concisely: If `s` is a set of points in an additive commutative group `V` over a division ring `k` such that the affine span of `s` has dimension at most 1, then adding any point `p` in the affine span of `s` to `s` maintains the collinearity of `s`.
|
Collinear.affineSpan_eq_of_ne
theorem Collinear.affineSpan_eq_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] {s : Set P},
Collinear k s → ∀ {p₁ p₂ : P}, p₁ ∈ s → p₂ ∈ s → p₁ ≠ p₂ → affineSpan k {p₁, p₂} = affineSpan k s
This theorem states that for a set of points in an affine space, if the set is collinear, then the affine span of any two distinct points from this set is equal to the affine span of the entire set. In other words, if a set of points all lie on a single line, then the subspace generated by any two distinct points from the set is the same as the subspace generated by the entire set.
More concisely: If a set of points in an affine space is collinear, then the affine span of any two distinct points is equal to the affine span of the entire set.
|
finite_of_fin_dim_affineIndependent
theorem finite_of_fin_dim_affineIndependent :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : FiniteDimensional k V] {p : ι → P},
AffineIndependent k p → Finite ι
The theorem `finite_of_fin_dim_affineIndependent` states that for any division ring `k`, any vector space `V` over `k`, any affine space `P` with `V` as its associated vector space, and any index set `ι`, given that `V` is finite-dimensional, if a family of points `p : ι → P` is affine-independent, then the index set `ι` must be finite.
In other words, in a finite-dimensional affine space, any collection of points that are affine-independent (meaning no nontrivial linear combination of them sums to zero) must be a finite set.
More concisely: In a finite-dimensional affine space, any affine-independent set of points is a finite set.
|
finrank_vectorSpan_insert_le
theorem finrank_vectorSpan_insert_le :
∀ {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),
FiniteDimensional.finrank k ↥(vectorSpan k (insert p ↑s)) ≤ FiniteDimensional.finrank k ↥s.direction + 1
This theorem states that for any division ring `k`, any additive commutative group `V`, any module `k V`, any torsor `V P`, any affine subspace `s` of `k P`, and any point `p` in `P`, adding a point `p` to a finite-dimensional subspace `s` can increase the rank of the subspace by at most one. In other words, the rank of the vector span of the set resulting from inserting a point `p` into the set of points generating the subspace `s` is less than or equal to the rank of the subspace `s` plus one. Here, "rank" refers to the finite dimension of the subspace or the vector span.
More concisely: For any division ring `k`, additive commutative group `V`, module `k V`, torsor `V/P`, affine subspace `s` of `k P`, and point `p` in `P`, the rank of the vector span of `s ∪ {p}` is at most the rank of `s` plus one.
|
collinear_insert_insert_of_mem_affineSpan_pair
theorem collinear_insert_insert_of_mem_affineSpan_pair :
∀ {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},
p₁ ∈ affineSpan k {p₃, p₄} → p₂ ∈ affineSpan k {p₃, p₄} → Collinear k {p₁, p₂, p₃, p₄}
The theorem states that given a division ring `k`, an additive commutative group `V`, a module `V` over `k`, an `V`-torsor `P`, and four points `p₁`, `p₂`, `p₃`, `p₄` of type `P`, if `p₁` and `p₂` both lie in the affine span of the points `p₃` and `p₄`, then the set of all four points `{p₁, p₂, p₃, p₄}` is collinear. This means that these four points all lie on the same straight line.
More concisely: Given a division ring `k`, an additive commutative group `V` with module structure over `k`, an `V`-torsor `P`, and four points `p₁, p₂, p₃, p₄` of type `P`, if `p₁` and `p₂` belong to the affine span of `p₃` and `p₄`, then `{p₁, p₂, p₃, p₄}` are collinear.
|
Collinear.subset
theorem Collinear.subset :
∀ {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₁ s₂ : Set P}, s₁ ⊆ s₂ → Collinear k s₂ → Collinear k s₁
The theorem `Collinear.subset` states that for any division ring `k`, additive commutative group `V`, and additive torsor `P` over `V`, if `s₁` and `s₂` are sets of points in `P`, and `s₁` is a subset of `s₂`, then if `s₂` is collinear (i.e., the dimension of the vector span of `s₂` is at most `1`), it follows that `s₁` is also collinear.
More concisely: Given a division ring `k`, an additive commutative group `V`, and an additive torsor `P` over `V`, if `s₁` is a subset of `s₂` in `P` and `s₂` is collinear, then `s₁` is also collinear.
|
coplanar_empty
theorem coplanar_empty :
∀ (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], Coplanar k ∅
The theorem `coplanar_empty` states that for all types `k`, `V`, `P`, given `k` is a division ring, `V` is an additive commutative group, `V` is a module over `k`, and `P` is a torsor for `V`, the empty set is coplanar. In other words, in any context of vector spaces (decided by the types `k`, `V`, and `P` and their instances), the empty set of points is always considered to be lying on the same plane, since the dimension of the vector span of the empty set is less than or equal to 2.
More concisely: In any context of a division ring `k`, an additive commutative group `V` that is a `k`-module, and a `V`-torsor `P`, the empty set of points in `P` is coplanar, i.e., its vector span has dimension less than or equal to 2.
|
AffineIndependent.card_le_card_of_subset_affineSpan
theorem AffineIndependent.card_le_card_of_subset_affineSpan :
∀ {k : Type u_1} {V : Type u_2} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
{s t : Finset V}, AffineIndependent k Subtype.val → ↑s ⊆ ↑(affineSpan k ↑t) → s.card ≤ t.card
This theorem states that if a finset, say 's', is affinely independent and is contained within the affine span of another finset, say 't', then the number of elements in 's' (its cardinality) is less than or equal to the number of elements in 't' (its cardinality). This holds under the conditions: type 'k' is a division ring, type 'V' forms an abelian (commutative) group under addition, and 'V' is a module over 'k'. Essentially, it's a statement about the relative size constraint that the affine independence of 's' and its containment in the affine span of 't' impose on the two sets.
More concisely: If 's' is a finset of elements in an abelian group 'V' over a division ring 'k' that is affinely independent and contained in the affine span of another finset 't', then the cardinality of 's' is less than or equal to the cardinality of 't'.
|
collinear_empty
theorem collinear_empty :
∀ (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], Collinear k ∅
The theorem `collinear_empty` states that for any DivisionRing `k`, any Additive Commutative Group `V`, any Type `P` and any module `V` over `k` with `P` being an Additive Torsor for `V`, the empty set is collinear. In other words, in such a setup, the empty set of points is considered to be lying on the same line, as the dimension of the vector span of the empty set is at most `1`.
More concisely: In the setting of a DivisionRing `k`, an Additive Commutative Group `V`, a Type `P`, and a `k`-module `V` with `P` being an Additive Torsor for `V`, the empty set of points in `P` is collinear due to having a vector span of at most dimension 1.
|
collinear_insert_insert_insert_left_of_mem_affineSpan_pair
theorem collinear_insert_insert_insert_left_of_mem_affineSpan_pair :
∀ {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₅ : P},
p₁ ∈ affineSpan k {p₄, p₅} →
p₂ ∈ affineSpan k {p₄, p₅} → p₃ ∈ affineSpan k {p₄, p₅} → Collinear k {p₁, p₂, p₃, p₄}
The theorem `collinear_insert_insert_insert_left_of_mem_affineSpan_pair` states that given five points `p₁`, `p₂`, `p₃`, `p₄`, and `p₅` within a division ring `k` and an associated module `V` over `k` and an affine torsor `P` over `V`, if `p₁`, `p₂`, and `p₃` all lie within the affine span of `p₄` and `p₅`, then the set of points `{p₁, p₂, p₃, p₄}` are collinear. In other words, if three points are in the smallest affine subspace containing two other points, then these four points are on the same line.
More concisely: Given points $p\_1, p\_2, p\_3, p\_4,$ and $p\_5$ in a division ring $k$ with associated module $V$ and affine torsor $P$ over $V$, if $p\_1, p\_2,$ and $p\_3$ lie in the affine span of $p\_4$ and $p\_5$, then $p\_1, p\_2, p\_3, p\_4$ are collinear.
|
Collinear.finrank_le_one
theorem Collinear.finrank_le_one :
∀ {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} [inst_4 : FiniteDimensional k ↥(vectorSpan k s)],
Collinear k s → FiniteDimensional.finrank k ↥(vectorSpan k s) ≤ 1
This theorem states that for any division ring `k`, additive commutative group `V`, and additively closed group `P`, and any set of points `s` with the property that the vector span over `k` is finite-dimensional, if the set of points is collinear, then the finite rank of the vector span over `k` is less than or equal to 1. This basically means that if a set of points in vector space is aligned along a single line (collinear), then the dimension of the subspace spanned by those points (their vector span) is at most 1.
More concisely: If a set of points in a vector space is collinear, then the dimension of their vector span is at most 1.
|
affineIndependent_iff_not_collinear_of_ne
theorem affineIndependent_iff_not_collinear_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 : Fin 3 → P} {i₁ i₂ i₃ : Fin 3},
i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → (AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃})
The theorem states that for any three distinct points, represented by `i₁`, `i₂`, and `i₃`, in a three-dimensional affine space over a field `k`, these points are affinely independent if and only if they are not collinear. Affine independence here means that no nontrivial combination of these points, where the coefficients sum to zero, results in zero. Collinearity means that the vector span of these points has dimension at most `1`, or in other words, the points all lie on the same line.
More concisely: Three distinct points in a three-dimensional affine space over a field are affinely independent if and only if they are not collinear.
|
coplanar_pair
theorem coplanar_pair :
∀ (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), Coplanar k {p₁, p₂}
The theorem `coplanar_pair` asserts that for any division ring `k`, additive commutative group `V`, and affine space `P` over `V`, any two points `p₁` and `p₂` in the space `P` are coplanar. In other words, the set containing just these two points is coplanar, which in this context is defined to mean that the vector span of the set has a rank (dimension) of at most `2`. This is always true because the vector space spanned by two points has dimension at most `1`.
More concisely: For any division ring `k`, additive commutative group `V`, and affine space `P` over `V`, any two points in `P` span a subspace of `P` of dimension at most 2.
|
affineIndependent_iff_not_finrank_vectorSpan_le
theorem affineIndependent_iff_not_finrank_vectorSpan_le :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] (p : ι → P) {n : ℕ},
Fintype.card ι = n + 2 →
(AffineIndependent k p ↔ ¬FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) ≤ n)
This theorem states that a set of `n + 2` points is affinely independent if and only if the vector span of these points does not have a dimension at most `n`. More specifically, given a division ring `k`, a module `V` over `k`, an affine torsor `P` over `V`, and a function `p` that maps each element from some finite type `ι` to a point in `P`, if the number of elements in `ι` (i.e., the number of points) is `n + 2`, then the points are affinely independent if the rank of the submodule spanned by the vector differences of these points is more than `n`. Here, affine independence means that no non-trivial weighted sum of the points, where the weights sum to zero, equals zero.
More concisely: A set of `n + 2` points in an affine space over a division ring is affinely independent if and only if the vector span of these points has dimension strictly greater than `n`.
|
Collinear.collinear_insert_iff_of_ne
theorem Collinear.collinear_insert_iff_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] {s : Set P},
Collinear k s →
∀ {p₁ p₂ p₃ : P}, p₂ ∈ s → p₃ ∈ s → p₂ ≠ p₃ → (Collinear k (insert p₁ s) ↔ Collinear k {p₁, p₂, p₃})
The theorem states that for a given collinear set of points of a certain type `P` in a module over a division ring `k`, if we have two distinct points `p₂` and `p₃` within this set, another point `p₁` will be collinear with the entire set if and only if `p₁` is also collinear with `p₂` and `p₃`. In other words, adding a point `p₁` to a collinear set maintains the collinearity of the set if and only if the point `p₁` is collinear with any two distinct points already in the set.
More concisely: A point is collinear with a given collinear set of points in a module over a division ring if and only if it is collinear with any two distinct points in the set.
|
Coplanar.finrank_le_two
theorem Coplanar.finrank_le_two :
∀ {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} [inst_4 : FiniteDimensional k ↥(vectorSpan k s)],
Coplanar k s → FiniteDimensional.finrank k ↥(vectorSpan k s) ≤ 2
The theorem `Coplanar.finrank_le_two` states that for a given set of points, if the vector span of these points (the submodule that contains all linear combinations of the differences between the points) is of finite dimension, then the property of being coplanar (the property where the vector span has a maximum dimension of 2) implies that the actual dimension of the vector span, quantified as a natural number, is less than or equal to 2. This theorem is an alias for the forward direction of another theorem, `coplanar_iff_finrank_le_two`, that posits the equivalence between being coplanar and having a vector span of dimension at most 2.
More concisely: If a set of points in a vector space has a finite-dimensional vector span, then the property of being coplanar (having a vector span of maximum dimension 2) implies that the actual dimension of the vector span is at most 2.
|
AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one
theorem AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : FiniteDimensional k V] [inst_5 : Fintype ι] {p : ι → P},
AffineIndependent k p → (affineSpan k (Set.range p) = ⊤ ↔ Fintype.card ι = FiniteDimensional.finrank k V + 1)
This theorem states that for a given finite affinely independent family of points, defined by a function `p : ι → P` mapping from an index set `ι` to a point space `P` over a division ring `k`, the affine span of this family spans the entire space (symbolized by `⊤`) if and only if the number of elements in the family (given by `Fintype.card ι`) is exactly one more than the rank of the finite-dimensional space `V` over `k` (given by `FiniteDimensional.finrank k V + 1`). In other words, an affine space is completely spanned by a set of points if the number of points is one greater than the dimension of the space.
More concisely: A finite affinely independent family of points in a finite-dimensional vector space over a division ring spans the entire space if and only if the number of points is one more than the space's dimension.
|
collinear_iff_exists_forall_eq_smul_vadd
theorem collinear_iff_exists_forall_eq_smul_vadd :
∀ {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),
Collinear k s ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
The theorem `collinear_iff_exists_forall_eq_smul_vadd` states that for a set of points `s` in a torsor space `P` over a division ring `k`, with the module `V` and additive commutative group structure on `V`, the set of points is collinear if and only if there exists a base point `p₀` and a vector `v` such that every point `p` in the set can be expressed as a scalar multiple of the vector `v` added to the base point `p₀`. In other words, all points in the set lie on the same line determined by the base point and the direction vector.
More concisely: For a set of points in a torsor space over a division ring with additive commutative group structure, the points are collinear if and only if there exists a base point and a vector such that every point is equal to the base point plus a scalar multiple of the vector.
|
collinear_iff_not_affineIndependent_set
theorem collinear_iff_not_affineIndependent_set :
∀ {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},
Collinear k {p₁, p₂, p₃} ↔ ¬AffineIndependent k ![p₁, p₂, p₃]
The theorem states that for any division ring `k`, an additive commutative group `V`, an add-torsor `P` and any three points `p₁`, `p₂`, and `p₃`, the points are collinear (that is, they all lie on the same straight line) if and only if they are not affinely independent. Here, a set of points is said to be affinely independent if and only if no nontrivial weighted subtraction of them (where the sum of weights is `0`) gives the zero vector; and a set of points is collinear if the vector span of these points has a dimension of at most `1`.
More concisely: For any division ring `k`, additive commutative group `V`, add-torsor `P`, and three points `p₁`, `p₂`, and `p₃` in `P`, they are collinear if and only if they are not affinely independent.
|
coplanar_of_fact_finrank_eq_two
theorem coplanar_of_fact_finrank_eq_two :
∀ {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) [h : Fact (FiniteDimensional.finrank k V = 2)],
Coplanar k s
The theorem `coplanar_of_fact_finrank_eq_two` states that for any set of points `s` in a vector space `V` equipped with a division ring `k`, an additive commutative group structure, and a module structure, and a torsor structure over `V` for the points `P`, if the finite rank of the vector space `V` over the division ring `k` is two (i.e., `V` is a two-dimensional space), then the set `s` of points is coplanar. In other words, if your space is two-dimensional, all your points inherently lie in the same plane.
More concisely: If a set of points in a two-dimensional vector space over a division ring is a torsor, then the points are coplanar.
|
AffineIndependent.finrank_vectorSpan_add_one
theorem AffineIndependent.finrank_vectorSpan_add_one :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] [inst_5 : Nonempty ι] {p : ι → P},
AffineIndependent k p → FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) + 1 = Fintype.card ι
The theorem `AffineIndependent.finrank_vectorSpan_add_one` states that for a finite affinely independent family (a family of points in which no nontrivial weighted subtractions, where the sum of weights is 0, are 0) represented by a function `p : ι → P`, the dimension of the subspace spanned by the differences of all pairs of points in the family (given by `vectorSpan k (Set.range p)`) is one less than the total number of points in the family (given by `Fintype.card ι`). This is expressed mathematically as: `FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) + 1 = Fintype.card ι`. In simpler terms, the dimension of the space spanned by differences of points in an affinely independent set is one less than the number of points in the set.
More concisely: The dimension of the subspace spanned by differences of points in a finite affinely independent set is one less than the number of points in the set.
|
coplanar_iff_finrank_le_two
theorem coplanar_iff_finrank_le_two :
∀ {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} [inst_4 : FiniteDimensional k ↥(vectorSpan k s)],
Coplanar k s ↔ FiniteDimensional.finrank k ↥(vectorSpan k s) ≤ 2
The theorem `coplanar_iff_finrank_le_two` states that for a given set of points `s` in a vector space over an arbitrary division ring `k`, the points are coplanar (i.e., all lying in the same plane) if and only if the `vectorSpan` of these points is finite-dimensional and its dimension is at most `2`. Here, `vectorSpan` refers to the submodule that spans the differences of the set of points. The dimensionality is measured using the `finrank` function, which returns the rank (or dimension) of a module as a natural number.
More concisely: The set of points in a vector space is coplanar if and only if the submodule spanned by their differences has finite rank at most 2.
|
affineIndependent_iff_finrank_vectorSpan_eq
theorem affineIndependent_iff_finrank_vectorSpan_eq :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] (p : ι → P) {n : ℕ},
Fintype.card ι = n + 1 →
(AffineIndependent k p ↔ FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) = n)
The theorem states that for a division ring `k`, an abelian additive group `V`, an affine torsor `P` over `V`, and a finite type `ι`, if you have `n + 1` points `p` (which is a function from `ι` to `P`) such that the number of elements in `ι` is `n + 1`, then these points are affinely independent if and only if the dimension of the vector span of the range of points `p` is `n`. In other words, for a given set of `n + 1` points, they are affinely independent (no nontrivial weighted subtractions of points are zero) exactly when the subspace spanned by the set of difference vectors of these points has a dimension of `n`.
More concisely: The theorem states that for a division ring `k`, an abelian additive group `V`, an affine torsor `P` over `V`, and a finite type `ι` with `n + 1` points `p : ι → P`, the points are affinely independent if and only if the dimension of the vector span of `p` is equal to `n`.
|
finite_set_of_fin_dim_affineIndependent
theorem finite_set_of_fin_dim_affineIndependent :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : FiniteDimensional k V] {s : Set ι} {f : ↑s → P},
AffineIndependent k f → s.Finite
This theorem states that for any Division Ring `k`, an affine space `P` over vector space `V`, and an indexing set `ι`. If `f` is a family of points in the affine space `P` indexed by elements of the set `s`, and this family of points is affine-independent, then provided that the vector space `V` is finite-dimensional over `k`, the set `s` must be finite. In other words, an affine-independent subset of a finite-dimensional affine space is always finite.
More concisely: In a finite-dimensional affine space over a division ring, every affine-independent set of points has a finite index set.
|
finrank_vectorSpan_image_finset_le
theorem finrank_vectorSpan_image_finset_le :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : DecidableEq P] (p : ι → P) (s : Finset ι) {n : ℕ},
s.card = n + 1 → FiniteDimensional.finrank k ↥(vectorSpan k ↑(Finset.image p s)) ≤ n
This theorem states that for any division ring `k`, and any additively commutative group `V` which is also a `k` vector space, and any affine space `P` over `V`, along with any function `p` from an index set `ι` to `P`, and a finite set `s` of indices in `ι` with `n + 1` elements, the dimension of the vector space spanned by the image of `s` under `p` is at most `n`. This dimension is calculated in the sense of finite-dimensional vector spaces, i.e., counting the maximum number of linearly independent vectors, with the convention that if the space is infinite-dimensional, the dimension is 0. The vector space spanned by a set of points in `P` is the set of all differences between points in the set.
More concisely: For any division ring `k`, additively commutative `k`-vector space `V`, affine space `P` over `V`, function `p` from an index set `ι` to `P`, and finite set `s` of `n+1` indices in `ι`, the dimension of the span of `p[s]` in `P` is at most `n`.
|
collinear_iff_not_affineIndependent
theorem collinear_iff_not_affineIndependent :
∀ {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 : Fin 3 → P},
Collinear k (Set.range p) ↔ ¬AffineIndependent k p
The theorem states that for any given Division Ring `k`, Additive Commutative Group `V`, and Additive Torsor `P`, and a function `p` mapping from the set of first 3 natural numbers (`Fin 3`) to `P`, three points (determined by the range of `p`) are collinear (i.e., they all lie on a straight line) if and only if they are not affinely independent. The term "affinely independent" here means that no nontrivial linear combination of the points, where the weights sum to zero, results in the zero vector.
More concisely: For any division ring `k`, additive commutative group `V`, additive torsor `P`, and function `p` mapping `Fin 3` to `P`, the three points in `P` corresponding to the range of `p` are collinear if and only if they are not affinely independent.
|
AffineIndependent.finrank_vectorSpan_image_finset
theorem AffineIndependent.finrank_vectorSpan_image_finset :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : DecidableEq P] {p : ι → P},
AffineIndependent k p →
∀ {s : Finset ι} {n : ℕ},
s.card = n + 1 → FiniteDimensional.finrank k ↥(vectorSpan k ↑(Finset.image p s)) = n
The theorem `AffineIndependent.finrank_vectorSpan_image_finset` states that for any Division Ring `k`, Additive Commutative Group `V`, Additive Torsor `P`, and `ι`, if we have an affinely independent family `p : ι → P`, then for any finite set `s` of type `ι` and a natural number `n`, if the cardinality of `s` is `n + 1`, then the dimension (or rank) of the `vectorSpan` (submodule spanning the differences) of the image of `s` under `p` is `n`. In simpler terms, the dimension of the vector space spanned by a finite subset of an affinely independent set is one less than the number of points in that subset.
More concisely: For any division ring `k`, additive commutative group `V`, additive torsor `P`, and affinely independent family `p : ι -> P`, the dimension of `vectorSpan {p i | i ∈ s}` is `n` when `s` is a finite subset of `ι` with `n + 1` elements.
|
collinear_iff_of_mem
theorem collinear_iff_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 : Set P} {p₀ : P},
p₀ ∈ s → (Collinear k s ↔ ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀)
The theorem `collinear_iff_of_mem` states that for any division ring `k`, any additively commutative group `V`, and any affine space `P` over `V`, if a point `p₀` is an element of a set of points `s`, then `s` is collinear (all points lie on a single line) if and only if all points in `s` can be represented as a scalar multiple of the same vector `v`, added to `p₀`. In mathematical terms, it says that a set of points is collinear if and only if each point `p` in the set can be written in the form `p = r * v + p₀` for some scalar `r`.
More concisely: A set of points in an affine space over a division ring is collinear if and only if every point in the set can be expressed as a scalar multiple of a fixed vector, added to a fixed point.
|
collinear_pair
theorem collinear_pair :
∀ (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), Collinear k {p₁, p₂}
The theorem `collinear_pair` states that, for any given division ring `k`, commutative additive group `V`, and additive torsor `P`, along with any two points `p₁` and `p₂` from `P`, these two points are collinear. Here, being collinear means that the vector span of the set containing these two points, when considered as a module over the division ring, has a rank less than or equal to `1`.
More concisely: Given a division ring `k`, a commutative additive group `V`, and an additive torsor `P` over `V`, any two points `p₁, p₂ ∈ P` are collinear, that is, their vector span over `k` has rank at most 1.
|
Collinear.coplanar_insert
theorem Collinear.coplanar_insert :
∀ {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}, Collinear k s → ∀ (p : P), Coplanar k (insert p s)
The theorem named `Collinear.coplanar_insert` states that for any Division Ring `k`, Additive Commutative Group `V`, and Additive Torsor `P`, if a set `s` of points in `P` is collinear (i.e., all points lie on a single straight line), then for any point `p` in `P`, the set obtained by adding `p` to `s` is coplanar (i.e., all points lie on a single plane). This theorem confirms the geometric intuition that adding a point to a line (a one-dimensional object) possibly results in a plane (a two-dimensional object).
More concisely: For any division ring `k`, additive commutative group `V`, and additive torsor `P` over `V`, if a finite subset `s` of `P` is collinear, then `s ∪ {p}` is coplanar for all `p` in `P`.
|
affineIndependent_iff_not_collinear
theorem affineIndependent_iff_not_collinear :
∀ {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 : Fin 3 → P},
AffineIndependent k p ↔ ¬Collinear k (Set.range p)
The theorem `affineIndependent_iff_not_collinear` states that for any three points in an affine space, these points are affinely independent if and only if they are not collinear. Here, affinely independent points are ones where no nontrivial weighted subtraction (where the sum of weights is zero) results in zero, and points being collinear means that their vector span has dimension at most one. The theorem applies to a scenario where the points are represented in a space characterized by its ring, additive commutative group, module, and add torsor structures.
More concisely: Three points in an affine space are affinely independent if and only if they are not collinear.
|
coplanar_singleton
theorem coplanar_singleton :
∀ (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), Coplanar k {p}
This theorem states that a single point is coplanar. In other words, in any division ring `k` and for any types `V` and `P` where `V` is an additive commutative group, `V` is a module over `k`, and `V` is an additive torsor for `P`, for any point `p` of type `P`, the set containing only `p` is coplanar. Here, a set of points being coplanar means that the dimension of the vector span of the set in the module is less than or equal to `2`.
More concisely: In any division ring `k` and for any additive commutative group `V` that is a module over `k` and an additive torsor for some type `P`, the singleton set of any point `p` in `P` has dimension at most 2 in `V`.
|
Collinear.finiteDimensional_direction_affineSpan
theorem Collinear.finiteDimensional_direction_affineSpan :
∀ {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},
Collinear k s → FiniteDimensional k ↥(affineSpan k s).direction
The theorem `Collinear.finiteDimensional_direction_affineSpan` states that for any division ring `k`, additive commutative group `V`, and affine torsor `P` over `V`, given a set `s` of points in `P`, if the set of points `s` is collinear, then the direction of the affine span of the set `s` is a finite-dimensional space over the division ring `k`. This indicates that the set of vectors defining the direction of the affine span, which is the smallest affine subspace containing the set of collinear points `s`, has a finite basis in the division ring `k`.
More concisely: If a set of points in an affine torsor over a division ring is collinear, then the direction of their affine span is a finite-dimensional space over that division ring.
|
finrank_vectorSpan_range_add_one_le
theorem finrank_vectorSpan_range_add_one_le :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] [inst_5 : Nonempty ι] (p : ι → P),
FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) + 1 ≤ Fintype.card ι
This theorem states that for an indexed family of points `p : ι → P` in an affine space `P` over a division ring `k`, the vector span of this family (which is a subspace of the vector space `V`) has a dimension which is at most one less than the number of points in the indexed family. In other words, if the family contains `n + 1` points, the vector span of these points has a dimension at most `n`. This captures the intuitive geometric idea that `n+1` points in a general position (no `n+1` points lie on the same `n-1` dimensional hyperplane) in an affine space determine an `n`-dimensional simplex.
More concisely: For an indexed family of points `p : ι → P` in an affine space `P` over a division ring `k`, the dimension of their vector span is at most `n`, where `n` is the number of points in the family.
|
collinear_iff_finrank_le_one
theorem collinear_iff_finrank_le_one :
∀ {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} [inst_4 : FiniteDimensional k ↥(vectorSpan k s)],
Collinear k s ↔ FiniteDimensional.finrank k ↥(vectorSpan k s) ≤ 1
This theorem, `collinear_iff_finrank_le_one`, states that for any given set of points `s` from a type `P`, within a vector space `V` over a division ring `k` (where vector `V` is an additive commutative group and `P` is a torsor for `V`), the set of points `s` is collinear if and only if the finite rank of the vector span of `s` (considered as a module over `k`) is less than or equal to `1`. This condition holds when the vector span of `s` is known to be finite-dimensional over the ring `k`. In other words, a set of points lies on a single line if and only if the dimension of the vector space spanned by their pairwise differences is at most `1`, provided that this vector space is finite-dimensional.
More concisely: A set of points in a vector space is collinear if and only if the rank of their span is at most 1.
|
Collinear.finiteDimensional_vectorSpan
theorem Collinear.finiteDimensional_vectorSpan :
∀ {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},
Collinear k s → FiniteDimensional k ↥(vectorSpan k s)
This theorem states that for any division ring `k`, additive commutative group `V`, and add-torsor `P`, if a set `s` of type `P` is collinear (meaning the vector span of the points has dimension at most 1), then the vector span of the collinear points is finite-dimensional over the division ring `k`. In other words, the vector space formed by taking linear combinations of the vectors between pairs of collinear points is a finite-dimensional vector space.
More concisely: For any division ring `k`, additive commutative group `V`, and add-torsor `P` over `V`, if a subset `s` of `P` is collinear, then the vector span of `s` is finite-dimensional over `k`.
|
affineIndependent_iff_le_finrank_vectorSpan
theorem affineIndependent_iff_le_finrank_vectorSpan :
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] (p : ι → P) {n : ℕ},
Fintype.card ι = n + 1 →
(AffineIndependent k p ↔ n ≤ FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)))
The theorem `affineIndependent_iff_le_finrank_vectorSpan` states that for a given division ring `k`, an `AddCommGroup` `V`, a module `V` over `k`, and an `AddTorsor` `V` over `P`, with `P` being a function of type `ι → P` where `ι` is a `Fintype`, and a given natural number `n`, if the cardinality of `ι` is `n + 1`, then the set of `n + 1` points defined by `P` is affinely independent if and only if the dimension of the vector span of the set of points is at least `n`. Here, the dimension is computed as the rank of the module, turned into a natural number, of the vector space spanned by the differences of all pairs of points in the set. Affine independence of a set of points means that no nontrivial weighted average of the points is equal to zero.
More concisely: For a division ring `k`, an `AddCommGroup` `V` over `k`, a module `V` over `k`, an `AddTorsor` `V` over a function `P` of type `ι → P` on a finite set `ι` of size `n+1`, the points defined by `P` are affinely independent if and only if the dimension of their vector span is at least `n`, where dimension is the rank of the module of the differences between all pairs of points.
|
collinear_insert_of_mem_affineSpan_pair
theorem collinear_insert_of_mem_affineSpan_pair :
∀ {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₁ ∈ affineSpan k {p₂, p₃} → Collinear k {p₁, p₂, p₃}
This theorem states that, given a specific division ring `k`, an additive commutative group `V`, a module `k V`, and an additive torsor `V P`, if a point `p₁` lies within the affine span of two other points `p₂` and `p₃` (i.e., `p₁` can be expressed as a linear combination of `p₂` and `p₃`), then these three points `p₁`, `p₂`, and `p₃` are collinear. "Collinear" here means that the vector span of these points has a dimension of at most `1`, or in other words, they all lie on the same line.
More concisely: Given a division ring `k`, an additive commutative group `V`, a module `k V`, and an additive torsor `V P`, if a point `p₁` lies in the affine span of points `p₂` and `p₃`, then `p₁`, `p₂`, and `p₃` are collinear. (Collinearity implies that their vector span has dimension at most 1.)
|
ne₂₃_of_not_collinear
theorem ne₂₃_of_not_collinear :
∀ {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}, ¬Collinear k {p₁, p₂, p₃} → p₂ ≠ p₃
The theorem "ne₂₃_of_not_collinear" states that in a division ring with an associated additive commutative group and a module, for any three points (p₁, p₂, p₃), if these points are not collinear (i.e., they do not all lie on the same straight line, or equivalently the vector span of these points has a dimension greater than 1), then the second and third points must be distinct, or in other words, p₂ is not equal to p₃.
More concisely: In a division ring with an additive commutative group and a module, if three points are not collinear, then they are pairwise distinct.
|
ne₁₂_of_not_collinear
theorem ne₁₂_of_not_collinear :
∀ {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}, ¬Collinear k {p₁, p₂, p₃} → p₁ ≠ p₂
The theorem `ne₁₂_of_not_collinear` states that given a division ring `k`, an additive commutative group `V`, a module `V` over `k`, and an additive torsor `P` over `V`, if three points `p₁`, `p₂` and `p₃` in `P` are not collinear (meaning the vector span of these points does not have a rank less than or equal to 1), then the first point `p₁` and the second point `p₂` must be distinct, or, in other words, `p₁` is not equal to `p₂`.
More concisely: If three distinct points in an additive torsor over an additive commutative group form a linearly independent set in their vector span over a division ring, then they are pairwise distinct.
|
affineIndependent_iff_not_collinear_set
theorem affineIndependent_iff_not_collinear_set :
∀ {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},
AffineIndependent k ![p₁, p₂, p₃] ↔ ¬Collinear k {p₁, p₂, p₃}
The theorem `affineIndependent_iff_not_collinear_set` states that, for any division ring `k`, additive commutative group `V`, and torsor `P` over `V` with `k`, and for any three points `p₁`, `p₂`, and `p₃` in `P`, these three points are affinely independent if and only if they are not collinear. Here, a set of points is said to be affinely independent if no nontrivial weighted subtractions (where the sum of weights is 0) result in 0, and a set of points is said to be collinear if the dimension of their vector span is at most 1.
More concisely: For any division ring `k`, additive commutative group `V`, and torsor `P` over `V` with `k`, three points `p₁`, `p₂`, and `p₃` in `P` are affinely independent if and only if they are not collinear, that is, their vector span has dimension at most 1 if and only if there exist weights `w₁, w₂, w₃ ≠ 0` such that `w₁p₁ + w₂p₂ + w₃p₃ = 0`.
|
Coplanar.subset
theorem Coplanar.subset :
∀ {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₁ s₂ : Set P}, s₁ ⊆ s₂ → Coplanar k s₂ → Coplanar k s₁
The theorem `Coplanar.subset` states that if we have a set of points `s₁` which is a subset of another set of points `s₂`, and if `s₂` is coplanar, then `s₁` is also coplanar. In the mathematical context, a set of points is said to be coplanar if the vector space spanned by them has a dimension of at most `2`. Hence, if `s₂` is such that its span has dimension at most `2` (i.e., it is coplanar), then any subset `s₁` of `s₂` will also have its span of dimension at most `2` (i.e., it will also be coplanar). The types `k`, `V`, `P` represent a division ring, an additive commutative group, and an affine space respectively, with `V` being a module over `k` and `P` being an affine space over `V`.
More concisely: If a subset `s₁` of a coplanar set `s₂` of points in an affine space over a division ring `k` and its module `V`, then `s₁` is also coplanar.
|
finrank_vectorSpan_insert_le_set
theorem finrank_vectorSpan_insert_le_set :
∀ (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) (p : P),
FiniteDimensional.finrank k ↥(vectorSpan k (insert p s)) ≤ FiniteDimensional.finrank k ↥(vectorSpan k s) + 1
The theorem `finrank_vectorSpan_insert_le_set` states that for any division ring `k`, any additive commutative group `V`, any set of points `P` that forms an additive torsor over `V`, and any point `p` and set `s` in `P`, the rank (or finite dimension) of the vector space spanned by the points obtained by inserting `p` into `s` is less than or equal to the rank of the vector space spanned by the points in `s` plus one. This essentially means that when you add a new point to a set, the dimension of the space spanned by the set increases by at most one.
More concisely: For any division ring K, additive commutative group V, additive torsor P over V, and points p in P and s in P, the rank of the vector space spanned by p and the points in s is less than or equal to the rank of the vector space spanned by the points in s plus one.
|
coplanar_triple
theorem coplanar_triple :
∀ (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), Coplanar k {p₁, p₂, p₃}
The theorem `coplanar_triple` states that for any three points (p₁, p₂, p₃) in an affine space over a division ring `k` with an associated vector space of type `V` and a point space of type `P`, these three points are always coplanar. Here, "coplanar" is defined such that a set of points is coplanar if the dimension of the vector span of this set is at most two.
More concisely: The theorem `coplanar_triple` asserts that any three points in an affine space over a division ring with associated vector space and point space have a vector span of dimension at most 2.
|
finiteDimensional_direction_affineSpan_of_finite
theorem finiteDimensional_direction_affineSpan_of_finite :
∀ (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},
s.Finite → FiniteDimensional k ↥(affineSpan k s).direction
This theorem states that for any division ring `k`, additive commutative group `V`, module `k` over `V`, and additive torsor `V` over `P`, the affine span of a finite set `s` of type `Set P` has a direction that is finite-dimensional over `k`. In simpler language, it asserts that the direction of the smallest affine subspace containing a finite set of points is a finite-dimensional vector space.
More concisely: Given a division ring `k`, an additive commutative group `V` made into a `k`-module and an additive torsor over a prime subgroup `P` of `V`, the affine hull of any finite set in `V` has finite dimension as a `k`-vector space.
|
collinear_iff_rank_le_one
theorem collinear_iff_rank_le_one :
∀ (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), Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
The theorem `collinear_iff_rank_le_one` states that for any division ring `k`, additive commutative group `V`, and `P` an additive torsor over `V`, the set of points `s` is collinear if and only if the rank of the submodule spanning the differences of the set of points (i.e., `vectorSpan`) is less than or equal to one. In mathematical terms, this means that the points in a set are in a straight line if the dimension of the space spanned by the vectors formed by their differences is at most one.
More concisely: For any additive torsor P over a commutative group V in a division ring k, the points in P are collinear if and only if the rank of the submodule spanned by the differences of these points is at most 1.
|
Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional._auxLemma.10
theorem Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional._auxLemma.10 :
∀ (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), Collinear k {p₁, p₂} = True
The theorem `Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional._auxLemma.10` states that for any division ring `k`, additively commutative group `V`, torsor `P` over `V`, and any two points `p₁` and `p₂` from `P`, the set containing only `p₁` and `p₂` is collinear. Recall that a set of points is defined to be collinear if the vector span of these points has a dimension at most `1`. In this case, the set of two points always forms a line (or is a point if the two points coincide) and thus is always collinear.
More concisely: For any division ring `k`, additively commutative group `V`, and torsor `P` over `V`, any two points `p₁` and `p₂` in `P` form a collinear set in the affine space of `P` over `k`.
|
AffineIndependent.finrank_vectorSpan
theorem AffineIndependent.finrank_vectorSpan :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] {p : ι → P},
AffineIndependent k p →
∀ {n : ℕ}, Fintype.card ι = n + 1 → FiniteDimensional.finrank k ↥(vectorSpan k (Set.range p)) = n
This theorem states that for any Division Ring `k`, Additive Commutative Group `V`, Additive Torsor `P`, and any finite type `ι`, given a function `p` from `ι` to `P` that forms an affinely independent set, the rank (or the dimension for a vector space over a field) of the `vectorSpan` (the submodule spanning the differences) of the range of `p` is one less than the cardinality (or the number of elements) of `ι`. In essence, the dimension of the spanned space of a finite affinely independent set is one less than the number of elements in the set.
More concisely: For any division ring `k`, additive commutative group `V`, additive torsor `P`, and finite type `ι`, the rank of `vectorSpan` over `k` of an affinely independent set of `ι` elements from `P` is one less than the cardinality of `ι`.
|
AffineIndependent.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one
theorem AffineIndependent.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : DecidableEq P] {p : ι → P},
AffineIndependent k p →
∀ {s : Finset ι} {sm : Submodule k V} [inst_5 : FiniteDimensional k ↥sm],
vectorSpan k ↑(Finset.image p s) ≤ sm →
s.card = FiniteDimensional.finrank k ↥sm + 1 → vectorSpan k ↑(Finset.image p s) = sm
The theorem `AffineIndependent.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one` states that if we have an affinely independent family \( p : \iota \rightarrow P \) in the context of a vector space over a division ring, and if we consider the `vectorSpan` of a finite subset of this family (obtained by applying the function `p` over a `Finset` `s` of indices), if this `vectorSpan` lies in a submodule `sm`, whose dimension is one less than the cardinality of the set `s`, then the `vectorSpan` is equal to the submodule `sm`. In other words, for an affinely independent family, if the dimension of the module spanned by a subset of the family is less by one than the size of the subset, the spanned module equals the containing module.
More concisely: Given an affinely independent family of vectors in a vector space over a division ring, if the span of a finite subset of the family has dimension one less than the size of the subset, then the span equals the containing submodule.
|
AffineIndependent.affineSpan_eq_of_le_of_card_eq_finrank_add_one
theorem AffineIndependent.affineSpan_eq_of_le_of_card_eq_finrank_add_one :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] {p : ι → P},
AffineIndependent k p →
∀ {sp : AffineSubspace k P} [inst_5 : FiniteDimensional k ↥sp.direction],
affineSpan k (Set.range p) ≤ sp →
Fintype.card ι = FiniteDimensional.finrank k ↥sp.direction + 1 → affineSpan k (Set.range p) = sp
This theorem states that given a finite family of points, represented by a function `p` from a finite type `ι` to a point type `P`, in a vector space over a division ring `k`, if this family of points is affinely independent, then for any affine subspace `sp` with finite dimension, if the affine span of the set of points defined by `p` is a subset of `sp`, and the cardinality of the finite type `ι` is one more than the rank of the direction of `sp`, then the affine span of the set of points defined by `p` equals `sp`.
In other words, for a set of affinely independent points, if the number of those points is one more than the dimension of a given subspace that contains them, then those points span the entire subspace.
More concisely: If a finite set of affinely independent points in a vector space over a division ring spans a subspace of dimension one less than their cardinality, then they span the entire subspace.
|
finiteDimensional_vectorSpan_of_finite
theorem finiteDimensional_vectorSpan_of_finite :
∀ (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}, s.Finite → FiniteDimensional k ↥(vectorSpan k s)
The theorem `finiteDimensional_vectorSpan_of_finite` states that for any division ring `k`, additive commutative group `V`, additive torsor `P`, and set `s` of type `P`, if the set `s` is finite, then the vector space spanned by the differences of any pairs of points in `s` (that is, the `vectorSpan` of `s`) is finite-dimensional over `k`. This means that there exists a finite number `n` such that there is a linear equivalence between `vectorSpan k s` and the `n`-dimensional vector space over `k`.
More concisely: If `k` is a division ring, `V` is an additive commutative group, `P` is an additive torsor over `V`, and `s` is a finite set in `P`, then the vector space spanned by the differences of pairs of points in `s` is finite-dimensional over `k`, with a dimension equal to some natural number.
|
collinear_insert_insert_insert_of_mem_affineSpan_pair
theorem collinear_insert_insert_insert_of_mem_affineSpan_pair :
∀ {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₅ : P},
p₁ ∈ affineSpan k {p₄, p₅} →
p₂ ∈ affineSpan k {p₄, p₅} → p₃ ∈ affineSpan k {p₄, p₅} → Collinear k {p₁, p₂, p₃, p₄, p₅}
The theorem `collinear_insert_insert_insert_of_mem_affineSpan_pair` states that given any division ring `k`, an additive commutative group `V`, a module of `V` over `k`, and an additive torsor of `V` for `P`, and five points `p₁`, `p₂`, `p₃`, `p₄`, `p₅` of `P`, if the points `p₁`, `p₂`, and `p₃` lie in the affine span of the points `p₄` and `p₅`, then all five points are collinear. In other words, if three points are in the smallest affine subspace containing two other points, all five points lie on a single line.
More concisely: If points $p\_1, p\_2, p\_3$ lie in the affine span of points $p\_4$ and $p\_5$, then $p\_1, p\_2, p\_3, p\_4, p\_5$ are collinear.
|
ne₁₃_of_not_collinear
theorem ne₁₃_of_not_collinear :
∀ {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}, ¬Collinear k {p₁, p₂, p₃} → p₁ ≠ p₃
The theorem `ne₁₃_of_not_collinear` states that for any division ring `k`, additively commutative group `V`, additively transitive group action `P`, and points `p₁`, `p₂`, `p₃` in `P`, if these three points are not collinear (i.e., they do not lie on the same line), then the first and third points (`p₁` and `p₃`) are not the same. This is expressed in Lean 4 as `¬Collinear k {p₁, p₂, p₃} → p₁ ≠ p₃`, which reads as "if it is not the case that the set `{p₁, p₂, p₃}` is collinear, then `p₁` is not equal to `p₃`".
More concisely: If three points in an additively transitive group action over an additively commutative group and division ring are not collinear, they are distinct.
|
collinear_iff_not_affineIndependent_of_ne
theorem collinear_iff_not_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 : Fin 3 → P} {i₁ i₂ i₃ : Fin 3},
i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → (Collinear k {p i₁, p i₂, p i₃} ↔ ¬AffineIndependent k p)
The theorem `collinear_iff_not_affineIndependent_of_ne` states that for any three distinct points in a division ring, represented by indices `i₁`, `i₂`, and `i₃`, these points are collinear (i.e., they all lie on the same straight line) if and only if they are not 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.
More concisely: Three distinct points in a division ring are collinear if and only if they are not affine independent.
|
AffineIndependent.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one
theorem AffineIndependent.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : DecidableEq P] {p : ι → P},
AffineIndependent k p →
∀ {s : Finset ι} {sp : AffineSubspace k P} [inst_5 : FiniteDimensional k ↥sp.direction],
affineSpan k ↑(Finset.image p s) ≤ sp →
s.card = FiniteDimensional.finrank k ↥sp.direction + 1 → affineSpan k ↑(Finset.image p s) = sp
The theorem `AffineIndependent.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one` states that if we have a family of points `p : ι → P` that are affinely independent over a division ring `k`, and a finite subset `s` of this family such that the affine span of this subset lies in an affine subspace `sp` whose direction is a vector space of dimension one less than the cardinality of `s`, then the affine span of the subset equals the affine subspace `sp`. This is contingent on the condition that the cardinality of `s` equals the rank of the vector space (`FiniteDimensional.finrank k ↥sp.direction`) plus one.
More concisely: If a family of points in a division ring is affinely independent and the affine span of a finite subset lies in an affine subspace of one lower dimension with a direction of the expected cardinality plus one, then the affine span equals the subspace.
|
collinear_singleton
theorem collinear_singleton :
∀ (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), Collinear k {p}
The theorem `collinear_singleton` states that for any single point `p`, belonging to an arbitrary type `P`, in a vector space `V` over a division ring `k`, the set containing just `p` is collinear. The vector space `V` is equipped with the structure of an additive commutative group and a `k`-module, and the type `P` is structured as an additive torsor over `V`. In simpler terms, this theorem proves that a set consisting of a single point is considered a collinear, as the vector space spanned by this set has a dimension less or equal to 1.
More concisely: For any point `p` in an additive torsor `P` over a vector space `V` with dimension less than or equal to 1, the set {`p`} is collinear.
|
Collinear.coplanar
theorem Collinear.coplanar :
∀ {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}, Collinear k s → Coplanar k s
The theorem `Collinear.coplanar` states that for any division ring `k`, an additive commutative group `V`, a set of points `P` where `V` acts freely and transitively on `P` (a torsor under `V`), and a set `s` of elements from `P`, if the set `s` is collinear (i.e., the dimension of the vector span of `s` over `k` is at most `1`), then `s` is also coplanar (i.e., the dimension of the vector span of `s` over `k` is at most `2`). This statement reflects the geometric idea that any set of points lying on a straight line (collinear points) also lie within a plane (coplanar points).
More concisely: If `s` is a set of points in a free and transitive action of an additive commutative group `V` over a division ring `k`, and `s` is collinear (i.e., the span of `s` over `k` has dimension at most 1), then `s` is coplanar (i.e., the span of `s` over `k` has dimension at most 2).
|
AffineIndependent.card_lt_card_of_affineSpan_lt_affineSpan
theorem AffineIndependent.card_lt_card_of_affineSpan_lt_affineSpan :
∀ {k : Type u_1} {V : Type u_2} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
{s t : Finset V}, AffineIndependent k Subtype.val → affineSpan k ↑s < affineSpan k ↑t → s.card < t.card
The theorem `AffineIndependent.card_lt_card_of_affineSpan_lt_affineSpan` states that for any division ring `k` and additive commutative group `V` with `V` being a `k`-module, given two finsets `s` and `t` of `V`, if the elements of `s` are affinely independent and the affine span of `s` is strictly contained within the affine span of `t`, then the cardinality of `s` is strictly less than the cardinality of `t`. In other words, if a set of points is affinely independent and its affine span is smaller than another set's affine span, then the first set must have fewer points than the second set.
More concisely: If `s` is an affinely independent set in a `k`-module `V` with strict inclusion of its affine span in the affine span of `t`, then the cardinality of `s` is strictly less than the cardinality of `t`.
|
collinear_triple_of_mem_affineSpan_pair
theorem collinear_triple_of_mem_affineSpan_pair :
∀ {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₅ : P},
p₁ ∈ affineSpan k {p₄, p₅} → p₂ ∈ affineSpan k {p₄, p₅} → p₃ ∈ affineSpan k {p₄, p₅} → Collinear k {p₁, p₂, p₃}
The theorem states that in a division ring `k` with an associated additive commutative group `V` and a module `V` on `k`, given any arbitrary points `p₁`, `p₂`, `p₃`, `p₄`, and `p₅` in an additively closed system (`AddTorsor`) `P`, if points `p₁`, `p₂`, and `p₃` lie in the smallest affine subspace (`affineSpan`) containing the points `p₄` and `p₅`, then the points `p₁`, `p₂`, and `p₃` are collinear. Here, "collinear" means that the vector space spanned by `p₁`, `p₂`, and `p₃` has a dimension of at most `1`.
More concisely: In a division ring with an associated additive commutative group and a module, if three points lie in the affine subspace spanning two other points in an additively closed system, then they are collinear.
|
coplanar_insert_iff_of_mem_affineSpan
theorem coplanar_insert_iff_of_mem_affineSpan :
∀ {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} {p : P},
p ∈ affineSpan k s → (Coplanar k (insert p s) ↔ Coplanar k s)
The theorem `coplanar_insert_iff_of_mem_affineSpan` states that for any Division Ring `k`, an Additive Commutative Group `V`, a Point `P` and a set of points `s`, if a point `p` is in the affine span of the set `s`, then adding `p` to the set `s` does not change the coplanarity of the set. In other words, a set of points `s` is coplanar if and only if the set `s` with an additional point `p`, which is in the affine span of `s`, is coplanar. The coplanarity of a set of points is determined by the condition that the dimension of their vector span is at most 2.
More concisely: For any division ring `k` and additive commutative group `V` with points `P`, `p` in `V`, and set `s` of points in `V` such that `p` is in the affine span of `s`, the set `s` is coplanar if and only if the set `s ∪ {p}` is coplanar.
|
coplanar_of_finrank_eq_two
theorem coplanar_of_finrank_eq_two :
∀ {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), FiniteDimensional.finrank k V = 2 → Coplanar k s
The theorem `coplanar_of_finrank_eq_two` states that for any set of points `s` in a vector space `V` over a division ring `k` (where the vector space `V` is equipped with the structure of an additive commutative group and a module over `k`, and a torsor structure under the additive action of `V`), if the rank (dimension) of the vector space `V` is equal to 2, then the set of points `s` is coplanar. The definition of coplanar here is such that the rank (dimension) of the span of the set of points is less than or equal to 2. This essentially means that if the space is two-dimensional, any set of points in that space lies on the same plane.
More concisely: If a set of points in a 2-dimensional vector space over a division ring forms a torsor under its additive action, then the points are coplanar, i.e., their span has dimension at most 2.
|
AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one
theorem AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one :
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
[inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : FiniteDimensional k V] [inst_5 : Fintype ι] {p : ι → P},
AffineIndependent k p → Fintype.card ι = FiniteDimensional.finrank k V + 1 → vectorSpan k (Set.range p) = ⊤
The theorem states that, given a division ring `k`, an additive commutative group `V`, an additive torsor `P` over `V`, a finite-dimensional module `V` over `k`, and a fintype `ι`, if we have an affine independent family `p` mapping elements of `ι` to points in `P` and the cardinality of this `ι` is one more than the rank of the `V` over `k`, then the vector span of the set of points generated by `p` spans the entire space, i.e., it's equal to `⊤`. In other words, for a set of points in a vector space that is affinely independent and size equal to the dimension of the space plus one, the span of those points covers the full space.
More concisely: If `k` is a division ring, `V` is a finite-dimensional additive commutative group, `P` is an additive torsor over `V`, and `p` is an affine-independent family of points in `P` of size one more than the rank of `V` over `k`, then the span of `p` equals the entire vector space `V`.
|