English
Let c be the inversion center, y another point, and R ≠ 0. The preimage of the perpendicular bisector of c and y under the inversion with center c and radius R is the sphere centered at the inverted point inv(c,R)(y) with radius R^2 / dist(y,c), with the center point c removed.
Русский
Пусть c — центр инверсии, y — произвольная точка, и R ≠ 0. Преобразование обратного образа (прообраз) перпендикулярной биссектору c и y под инверсией с центром c и радиусом R есть сфера с центром в inv(c,R)(y) и радиусом R^2 / dist(y,c), за исключением точки c.
LaTeX
$$$ \operatorname{Set.preimage}(\mathrm{inversion}(c,R), \perpBisector(c,y)) = \mathrm{sphere}(\mathrm{inversion}(c,R)\,y, \frac{R^{2}}{\operatorname{dist}(y,c)}) \setminus \{c\}$$$
Lean4
theorem preimage_inversion_perpBisector (hR : R ≠ 0) (hy : y ≠ c) :
inversion c R ⁻¹' perpBisector c y = sphere (inversion c R y) (R ^ 2 / dist y c) \ { c } := by
rw [← dist_inversion_center, ← preimage_inversion_perpBisector_inversion hR, inversion_inversion] <;> simp [*]
