inversion_mem_perpBisector_inversion_iff

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]

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