pointReflection_midpoint_right — Mathlib

English

In the affine setting, the point reflection about the midpoint of x and y sends x to y and y to x.

Русский

В афинной геометрии отражение точки относительно середины отрезка xy переводит x в y и y в x.

LaTeX

$$$\\text{pointReflection}_R(\\text{midpoint}_R x y)(x) = y$$$

Lean4

theorem pointReflection_midpoint_right (x y : P) : pointReflection R (midpoint R x y) y = x := by
  rw [midpoint_comm, AffineEquiv.pointReflection_midpoint_left]

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