inversion_mem_perpBisector_inversion_iff'

English

If R ≠ 0 and y ≠ c, inversion(c,R,x) ∈ perpBisector(c, inversion(c,R,y)) iff dist(x,y) = dist(y,c) and x ≠ c.

Русский

Если R ≠ 0 и y ≠ c, inversion(c,R,x) лежит на perpBisector(c, inversion(c,R,y)) тогда и только тогда, когда dist(x,y) = dist(y,c) и x ≠ c.

LaTeX

$$R ≠ 0 ∧ y ≠ c ⇒ (inversion(c,R,x) ∈ perpBisector(c, inversion(c,R,y)) ⇔ dist(x,y) = dist(y,c) ∧ x ≠ 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) (hy : y ≠ c) :
    inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c ∧ x ≠ c :=
  by
  rcases eq_or_ne x c with rfl | hx
  · simp [*]
  · simp [inversion_mem_perpBisector_inversion_iff hR hx hy, hx]

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