affineSegment_const_vadd_image — Mathlib

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

Похожие утверждения