mem_const_vadd_affineSegment — Mathlib

English

For any fixed vector v, z ∈ affineSegment(R, x, y) if and only if z+ᵥ v ∈ affineSegment(R, x+ᵥ v, y+ᵥ v).

Русский

При фиксированном векторе v: z ∈ affineSegment(R, x, y) тогда и только тогда, когда z+ᵥ v ∈ affineSegment(R, x+ᵥ v, y+ᵥ v).

LaTeX

$$$z\in\operatorname{affineSegment}(R,x,y) \iff z+ᵥ v \in \operatorname{affineSegment}(R,x+ᵥ v,y+ᵥ v).$$$

Lean4

@[simp]
theorem mem_const_vadd_affineSegment {x y z : P} (v : V) :
    v +ᵥ z ∈ affineSegment R (v +ᵥ x) (v +ᵥ y) ↔ z ∈ affineSegment R x y := by
  rw [← affineSegment_const_vadd_image, (AddAction.injective v).mem_set_image]

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