English
Let hR ≠ 0 and hy ≠ c. The preimage under inversion with center c and radius R of the sphere centered at y with radius dist(y,c) equals the set consisting of c together with the perpBisector of c and inv(c,R)y.
Русский
Пусть hR ≠ 0 и hy ≠ c. Преобразование инверсии с центром c и радиусом R обратимою образом сферы с центром y и радиусом dist(y,c) дает множество, состоящее из точки c и перпBisector(c, inv(c,R)y).
LaTeX
$$$ \operatorname{Set.preimage}(\mathrm{inversion}(c,R), \mathrm{sphere}(y, \operatorname{dist}(y,c))) = \{c\} \cup (\perpBisector(c, \mathrm{inversion}(c,R)\,y))$$$
Lean4
theorem preimage_inversion_sphere_dist_center (hR : R ≠ 0) (hy : y ≠ c) :
inversion c R ⁻¹' sphere y (dist y c) = insert c (perpBisector c (inversion c R y) : Set P) :=
by
ext x
rcases eq_or_ne x c with rfl | hx; · simp [dist_comm]
rw [mem_preimage, mem_sphere, ← inversion_mem_perpBisector_inversion_iff hR] <;> simp [*]