Betweenness in affine spaces #
This file defines notions of a point in an affine space being between two given points.
Main definitions #
affineSegment R x y
: The segment of points weakly betweenx
andy
.Wbtw R x y z
: The pointy
is weakly betweenx
andz
.Sbtw R x y z
: The pointy
is strictly betweenx
andz
.
The segment of points weakly between x
and y
. When convexity is refactored to support
abstract affine combination spaces, this will no longer need to be a separate definition from
segment
. However, lemmas involving +ᵥ
or -ᵥ
will still be relevant after such a
refactoring, as distinct from versions involving +
or -
in a module.
Equations
- affineSegment R x y = ⇑(AffineMap.lineMap x y) '' Set.Icc 0 1
Instances For
The point y
is weakly between x
and z
.
Equations
- Wbtw R x y z = (y ∈ affineSegment R x z)
Instances For
Alias of the reverse direction of mem_segment_iff_wbtw
.
Alias of the forward direction of wbtw_comm
.
Alias of the forward direction of sbtw_comm
.
Suppose lines from two vertices of a triangle to interior points of the opposite side meet at
p
. Then p
lies in the interior of the first (and by symmetry the other) segment from a
vertex to the point on the opposite side.
If T
is an affine independent family of points,
then any 3 distinct points form a triangle.