affineSegment_vadd_const_image — Mathlib

English

The image of the affine segment under the map z ↦ z +ᵥ p is the segment between x+ᵥp and y+ᵥp.

Русский

Образ афинного отрезка при отображении z ↦ z +ᵥ p равен отрезку между x+ᵥp и y+ᵥp.

LaTeX

$$$\left(\,\_ +ᵥ p\right)''\operatorname{affineSegment}(R,x,y) = \operatorname{affineSegment}(R,x+ᵥp,y+ᵥp).$$$

Lean4

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

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