midpoint_eq_midpoint_iff_vsub_eq_vsub

English

Equality of two midpoints is equivalent to equality of two corresponding v-subtractions: midpoint(R,x,y)=midpoint(R,x',y') iff x-ᵥ x' = y'-ᵥ y.

Русский

Равенство середин двух пар эквивалентно равенству их соответствующих векторных разностей: midpoint(R,x,y)=midpoint(R,x',y') ⇔ x-ᵥ x' = y'-ᵥ y.

LaTeX

$$$ \\operatorname{midpoint}(R,x,y) = \\operatorname{midpoint}(R,x',y') \\iff x -_{\\mathrm{v}} x' = y' -_{\\mathrm{v}} y $$$

Lean4

theorem midpoint_eq_midpoint_iff_vsub_eq_vsub {x x' y y' : P} : midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y :=
  by
  rw [← @vsub_eq_zero_iff_eq V, midpoint_vsub_midpoint, midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, zero_sub,
    vadd_eq_add, add_zero, neg_eq_iff_eq_neg, neg_vsub_eq_vsub_rev]

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