English
The affine segment between x and y in an affine space is the image of the closed interval [0,1] under the line map from x to y; equivalently, all affine combinations (1−t)x + t y with t ∈ [0,1].
Русский
Афинный отрезок между точками x и y в аффинном пространстве — образ замкнутого отрезка [0,1] под линейной картой от x к y; эквивалентно все аффинные комбинации (1−t)x + t y при t ∈ [0,1].
LaTeX
$$$\operatorname{affineSegment}(R,x,y) = \{(1-t)\,x + t\,y : t \in [0,1]\}$$$
Lean4
/-- 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. -/
def affineSegment [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : P) :=
lineMap x y '' Set.Icc (0 : R) 1
