English
The image of the affine segment under the map z ↦ z +ᵥ p equals the segment between z+x and z+y translated by p.
Русский
Образ афинного отрезка при отображении z ↦ z +ᵥ p равен отрезку между x+ᵥp и y+ᵥp после переноса.
LaTeX
$$$\left(p+\cdot\right)''\operatorname{affineSegment}(R,x,y) = \operatorname{affineSegment}(R,x+ᵥp,y+ᵥp).$$$
Lean4
@[simp]
theorem affineSegment_vsub_const_image (x y p : P) :
(· -ᵥ p) '' affineSegment R x y = affineSegment R (x -ᵥ p) (y -ᵥ p) :=
affineSegment_image ((AffineEquiv.vaddConst R p).symm : P →ᵃ[R] V) x y