midpoint_pointReflection_right

Mathlib.LinearAlgebra.AffineSpace.Midpoint

URI: https://scilib.ai/kg/mathlib#midpoint_pointReflection_right

English

The midpoint of y and the pointReflection of x by y equals x.

Русский

Средняя между y и отражением точки x относительно y равна x.

LaTeX

$$$ \\operatorname{midpoint}(R, y, \\operatorname{pointReflection}(R,x,y)) = x $$$

Lean4

@[simp]
theorem midpoint_pointReflection_right (x y : P) : midpoint R y (Equiv.pointReflection x y) = x :=
  midpoint_eq_iff.2 rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru