English
If x and y are not at the center c, then the distance between their images under inversion equals R^2 divided by the product dist(x,c) dist(y,c), times the distance dist(x,y).
Русский
Если x и y не равны центру c, то расстояние между изображениями(x) и изображениями(y) после инверсии равно $\frac{R^2}{dist(x,c)\, dist(y,c)}\, dist(x,y)$.
LaTeX
$$$x \ne c \land y \ne c \Rightarrow\ dist(\operatorname{inversion}(c,R,x), \ operatorname{inversion}(c,R,y)) = \dfrac{R^2}{\operatorname{dist}(x,c) \operatorname{dist}(y,c)} \cdot \operatorname{dist}(x,y)$$$
Lean4
/-- Distance between the images of two points under an inversion. -/
theorem dist_inversion_inversion (hx : x ≠ c) (hy : y ≠ c) (R : ℝ) :
dist (inversion c R x) (inversion c R y) = R ^ 2 / (dist x c * dist y c) * dist x y :=
by
dsimp only [inversion]
simp_rw [dist_vadd_cancel_right, dist_eq_norm_vsub V _ c]
simpa only [dist_vsub_cancel_right] using dist_div_norm_sq_smul (vsub_ne_zero.2 hx) (vsub_ne_zero.2 hy) R
