English
Translating both endpoints of an affine segment by a fixed vector v yields the image equal to the affine segment between the translated endpoints.
Русский
Смещение обеих концов афинного отрезка фиксированным вектором v дает образ, равный афинному отрезку между смещенными концами.
LaTeX
$$$\ (v +\cdot)\,\operatorname{affineSegment}(R,x,y) = \operatorname{affineSegment}(R,v+x,v+y).$$$
Lean4
@[simp]
theorem affineSegment_const_vadd_image (x y : P) (v : V) :
(v +ᵥ ·) '' affineSegment R x y = affineSegment R (v +ᵥ x) (v +ᵥ y) :=
affineSegment_image (AffineEquiv.constVAdd R P v : P →ᵃ[R] P) x y