preimage_inversion_perpBisector_inversion

English

The preimage of the perp bisector under inversion with center c and radius R (R ≠ 0) and y ≠ c is the set of points at distance dist(y,c) from y, excluding c.

Русский

Это множество точек на расстоянии dist(y,c) от y, исключая c, которое является прообразом perpBisector(c, inversion(c,R,y)) под inversion(c,R).

LaTeX

$$Set.preimage (inversion c R) (perpBisector c (inversion c R y)) = sphere(y, dist(y,c)) \ { c }$$

Lean4

theorem preimage_inversion_perpBisector_inversion (hR : R ≠ 0) (hy : y ≠ c) :
    inversion c R ⁻¹' perpBisector c (inversion c R y) = sphere y (dist y c) \ { c } :=
  Set.ext fun _ ↦ inversion_mem_perpBisector_inversion_iff' hR hy

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