affineSegment_const_vsub_image — Mathlib

English

As above, translating an affine segment by a fixed vector results in the translated segment between the translated endpoints.

Русский

Как выше, перенос афинного отрезка фиксированным вектором приводит к переносенному отрезку между переносимыми концами.

LaTeX

$$$\left(\,v+\cdot\right)''\operatorname{affineSegment}(R,x,y) = \operatorname{affineSegment}(R,v+x,v+y).$$$

Lean4

@[simp]
theorem affineSegment_const_vsub_image (x y p : P) :
    (p -ᵥ ·) '' affineSegment R x y = affineSegment R (p -ᵥ x) (p -ᵥ y) :=
  affineSegment_image (AffineEquiv.constVSub R p : P →ᵃ[R] V) x y

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