preimage_inversion_sphere_dist_center

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 [*]

Похожие утверждения