affineSegment_vsub_const_image — Mathlib

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

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