mem_const_vsub_affineSegment — Mathlib

English

For any p, z ∈ affineSegment(R, p−x, p−y) iff z ∈ affineSegment(R, x, y) after translating by p.

Русский

Для любого p: z ∈ affineSegment(R, p−x, p−y) тогда и только тогда, когда z в affineSegment(R, x, y) после переноса.

LaTeX

$$$z \in \operatorname{affineSegment}(R, p- x, p- y) \iff z \in \operatorname{affineSegment}(R, x, y).$$$

Lean4

@[simp]
theorem mem_const_vsub_affineSegment {x y z : P} (p : P) :
    p -ᵥ z ∈ affineSegment R (p -ᵥ x) (p -ᵥ y) ↔ z ∈ affineSegment R x y := by
  rw [← affineSegment_const_vsub_image, (vsub_right_injective p).mem_set_image]

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