image_inversion_sphere_dist_center

English

Let hR ≠ 0 and hy ≠ c. The image under inversion with center c and radius R of the sphere with center y and radius dist(y,c) equals the insert of c into the perpBisector c (inv(c,R) y).

Русский

Пусть hR ≠ 0 и hy ≠ c. Образ сферы с центром y и радиусом dist(y,c) под инверсией с центром в c и радиусом R равен добавлению c в перп биссектор c( inv(c,R)y ).

LaTeX

$$$ \mathrm{Set.image}(\mathrm{inversion}(c,R), \mathrm{sphere}(y, \operatorname{dist}(y,c))) = \mathrm{insert}\, c \, (\perpBisector(c, \mathrm{inversion}(c,R)\,y))$$$

Lean4

theorem image_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
  rw [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
    preimage_inversion_sphere_dist_center hR hy]

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