Finite-dimensional subspaces of affine spaces. #
This file provides a few results relating to finite-dimensional subspaces of affine spaces.
Main definitions #
Collinear
defines collinear sets of points as those that span a subspace of dimension at most 1.
The vectorSpan
of a finite set is finite-dimensional.
The vectorSpan
of a family indexed by a Fintype
is
finite-dimensional.
Equations
- ⋯ = ⋯
The vectorSpan
of a subset of a family indexed by a Fintype
is finite-dimensional.
Equations
- ⋯ = ⋯
The direction of the affine span of a finite set is finite-dimensional.
The direction of the affine span of a family indexed by a
Fintype
is finite-dimensional.
Equations
- ⋯ = ⋯
The direction of the affine span of a subset of a family indexed
by a Fintype
is finite-dimensional.
Equations
- ⋯ = ⋯
An affine-independent family of points in a finite-dimensional affine space is finite.
An affine-independent subset of a finite-dimensional affine space is finite.
The vectorSpan
of a finite subset of an affinely independent
family has dimension one less than its cardinality.
The vectorSpan
of a finite affinely independent family has
dimension one less than its cardinality.
The vectorSpan
of a finite affinely independent family has dimension one less than its
cardinality.
The vectorSpan
of a finite affinely independent family whose
cardinality is one more than that of the finite-dimensional space is
⊤
.
The vectorSpan
of n + 1
points in an indexed family has
dimension at most n
.
The vectorSpan
of an indexed family of n + 1
points has
dimension at most n
.
The vectorSpan
of an indexed family of n + 1
points has dimension at most n
.
n + 1
points are affinely independent if and only if their
vectorSpan
has dimension n
.
n + 1
points are affinely independent if and only if their
vectorSpan
has dimension at least n
.
n + 2
points are affinely independent if and only if their
vectorSpan
does not have dimension at most n
.
n + 2
points have a vectorSpan
with dimension at most n
if
and only if they are not affinely independent.
If an affine independent finset is contained in the affine span of another finset, then its cardinality is at most the cardinality of that finset.
If the affine span of an affine independent finset is strictly contained in the affine span of another finset, then its cardinality is strictly less than the cardinality of that finset.
If the vectorSpan
of a finite subset of an affinely independent
family lies in a submodule with dimension one less than its
cardinality, it equals that submodule.
If the vectorSpan
of a finite affinely independent
family lies in a submodule with dimension one less than its
cardinality, it equals that submodule.
If the affineSpan
of a finite subset of an affinely independent
family lies in an affine subspace whose direction has dimension one
less than its cardinality, it equals that subspace.
If the affineSpan
of a finite affinely independent family lies
in an affine subspace whose direction has dimension one less than its
cardinality, it equals that subspace.
The affineSpan
of a finite affinely independent family is ⊤
iff the
family's cardinality is one more than that of the finite-dimensional space.
The vectorSpan
of adding a point to a finite-dimensional subspace is finite-dimensional.
Equations
- ⋯ = ⋯
The direction of the affine span of adding a point to a finite-dimensional subspace is finite-dimensional.
Equations
- ⋯ = ⋯
The vectorSpan
of adding a point to a set with a finite-dimensional vectorSpan
is
finite-dimensional.
Equations
- ⋯ = ⋯
A set of points is collinear if their vectorSpan
has dimension
at most 1
.
Equations
- Collinear k s = (Module.rank k ↥(vectorSpan k s) ≤ 1)
Instances For
The definition of Collinear
.
A set of points, whose vectorSpan
is finite-dimensional, is
collinear if and only if their vectorSpan
has dimension at most
1
.
Alias of the forward direction of collinear_iff_finrank_le_one
.
A set of points, whose vectorSpan
is finite-dimensional, is
collinear if and only if their vectorSpan
has dimension at most
1
.
A subset of a collinear set is collinear.
The vectorSpan
of collinear points is finite-dimensional.
The direction of the affine span of collinear points is finite-dimensional.
The empty set is collinear.
A single point is collinear.
Given a point p₀
in a set of points, that set is collinear if and
only if the points can all be expressed as multiples of the same
vector, added to p₀
.
A set of points is collinear if and only if they can all be expressed as multiples of the same vector, added to the same base point.
Two points are collinear.
Three points are affinely independent if and only if they are not collinear.
Three points are collinear if and only if they are not affinely independent.
Three points are affinely independent if and only if they are not collinear.
Three points are collinear if and only if they are not affinely independent.
Three points are affinely independent if and only if they are not collinear.
Three points are collinear if and only if they are not affinely independent.
If three points are not collinear, the first and second are different.
If three points are not collinear, the first and third are different.
If three points are not collinear, the second and third are different.
A point in a collinear set of points lies in the affine span of any two distinct points of that set.
The affine span of any two distinct points of a collinear set of points equals the affine span of the whole set.
Given a collinear set of points, and two distinct points p₂
and p₃
in it, a point p₁
is
collinear with the set if and only if it is collinear with p₂
and p₃
.
Adding a point in the affine span of a set does not change whether that set is collinear.
If a point lies in the affine span of two points, those three points are collinear.
If two points lie in the affine span of two points, those four points are collinear.
If three points lie in the affine span of two points, those five points are collinear.
If three points lie in the affine span of two points, the first four points are collinear.
If three points lie in the affine span of two points, the first three points are collinear.
A set of points is coplanar if their vectorSpan
has dimension at most 2
.
Equations
- Coplanar k s = (Module.rank k ↥(vectorSpan k s) ≤ 2)
Instances For
The vectorSpan
of coplanar points is finite-dimensional.
The direction of the affine span of coplanar points is finite-dimensional.
A set of points, whose vectorSpan
is finite-dimensional, is coplanar if and only if their
vectorSpan
has dimension at most 2
.
Alias of the forward direction of coplanar_iff_finrank_le_two
.
A set of points, whose vectorSpan
is finite-dimensional, is coplanar if and only if their
vectorSpan
has dimension at most 2
.
A subset of a coplanar set is coplanar.
Collinear points are coplanar.
The empty set is coplanar.
A single point is coplanar.
Two points are coplanar.
Adding a point in the affine span of a set does not change whether that set is coplanar.
Adding a point to a finite-dimensional subspace increases the dimension by at most one.
Adding a point to a set with a finite-dimensional span increases the dimension by at most one.
Adding a point to a collinear set produces a coplanar set.
A set of points in a two-dimensional space is coplanar.
A set of points in a two-dimensional space is coplanar.
Three points are coplanar.