image_inversion_perpBisector — Mathlib

English

Let c ∈ P, y ∈ P, and R ≠ 0. The image of the perpBisector of c and y under the inversion with center c and radius R is the sphere centered at inv(c,R)(y) with radius R^2 / dist(y,c), with the center point c removed.

Русский

Пусть c, y ∈ P и R ≠ 0. Образ перп-биссектора c и y при инверсии с центром в c и радиусом R есть сфера с центром в inv(c,R)(y) и радиусом R^2 / dist(y,c), за исключением точки c.

LaTeX

$$$ \mathrm{Set.image}(\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 image_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 [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
    preimage_inversion_perpBisector hR hy]

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