mem_vsub_const_affineSegment — Mathlib

English

For any z, z +ᵥ p ∈ affineSegment(R, x, y) iff z ∈ affineSegment(R, x−ᵥ p, y−ᵥ p).

Русский

Для любого z: z+ᵥ p ∈ affineSegment(R, x, y) тогда и только тогда, когда z ∈ affineSegment(R, x−ᵥ p, y−ᵥ p).

LaTeX

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

Lean4

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

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