English
Distance from the center to the inverted point equals R^2 divided by the distance from the center to the original point.
Русский
Расстояние от центра до инверсии равно R^2/dist(x,c).
LaTeX
$$$\operatorname{dist}(c, \operatorname{inversion}(c,R)x) = \dfrac{R^2}{\operatorname{dist}(x,c)}$$$
Lean4
@[simp]
theorem inversion_inversion (c : P) {R : ℝ} (hR : R ≠ 0) (x : P) : inversion c R (inversion c R x) = x :=
by
rcases eq_or_ne x c with (rfl | hne)
· rw [inversion_self, inversion_self]
· rw [inversion, dist_inversion_center, inversion_vsub_center, smul_smul, ← mul_pow, div_mul_div_comm,
div_mul_cancel₀ _ (dist_ne_zero.2 hne), ← sq, div_self, one_pow, one_smul, vsub_vadd]
exact pow_ne_zero _ hR