English
For nonzero R and x,y not equal to c, inversion(c,R,x) lies in the perpendicular bisector of c and inversion(c,R,y) iff dist(x,y) = dist(y,c).
Русский
При R ≠ 0 и x,y ≠ c, inversion(c,R,x) лежит на перпендикулярной биссектрисе отрезка c–inversion(c,R,y) тогда и только тогда, когда dist(x,y) = dist(y,c).
LaTeX
$$R ≠ 0 ∧ x ≠ c ∧ y ≠ c ⇒ inversion(c,R,x) ∈ perpBisector(c, inversion(c,R,y)) ⇔ dist(x,y) = dist(y,c)$$
Lean4
/-- The inversion with center `c` and radius `R` maps a sphere passing through the center to a
hyperplane. -/
theorem inversion_mem_perpBisector_inversion_iff (hR : R ≠ 0) (hx : x ≠ c) (hy : y ≠ c) :
inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c :=
by
rw [mem_perpBisector_iff_dist_eq, dist_inversion_inversion hx hy, dist_inversion_center]
simp [field, eq_comm, ↓hx, ↓hy]