mem_vadd_const_affineSegment — Mathlib

English

The image of an affine segment under z ↦ p − z equals the affine segment between p−x and p−y.

Русский

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

LaTeX

$$$(p -\cdot)''\operatorname{affineSegment}(R,x,y) = \operatorname{affineSegment}(R,p- x,p- y).$$$

Lean4

@[simp]
theorem mem_vadd_const_affineSegment {x y z : V} (p : P) :
    z +ᵥ p ∈ affineSegment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affineSegment R x y := by
  rw [← affineSegment_vadd_const_image, (vadd_right_injective p).mem_set_image]

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