dist_right_pointReflection — Mathlib

English

The distance from q to the point reflection of p about q equals 2 times the distance between p and q.

Русский

Расстояние от q до отображения точки p через отражение относительно q равно 2·dist(p,q).

LaTeX

$$$\mathrm{dist}\; q\; (\mathrm{Equiv.pointReflection}\; p\; q) = ‖2‖ \cdot \mathrm{dist}\; p\; q$$$

Lean4

theorem dist_right_pointReflection (p q : P) : dist q (Equiv.pointReflection p q) = ‖(2 : 𝕜)‖ * dist p q :=
  (dist_comm _ _).trans (dist_pointReflection_right 𝕜 _ _)

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