English
Distance formula relating center, inverted image, and original point, with symmetry under center changes.
Русский
Расстояние между центром и инвертированным изображением связано с исходной точкой через симметрию по центру.
LaTeX
$$$\text{(distance relation; see 117295)}$$$
Lean4
/-- Distance from the image of a point under inversion to the center. This formula accidentally
works for `x = c`. -/
theorem dist_inversion_center (c x : P) (R : ℝ) : dist (inversion c R x) c = R ^ 2 / dist x c :=
by
rcases eq_or_ne x c with (rfl | hx)
· simp
have : dist x c ≠ 0 := dist_ne_zero.2 hx
simp only [inversion]
field_simp
simp only [sq, dist_vadd_left, norm_smul, norm_div, norm_mul, Real.norm_eq_abs, abs_mul_abs_self, abs_dist,
← dist_eq_norm_vsub]
field_simp