dist_inversion_center — Mathlib

English

Distance formula relating center, inverted image, and original point, with symmetry under center changes.

Русский

Расстояние между центром и инвертированным изображением связано с исходной точкой через симметрию по центру.

LaTeX

$$$\text{(distance relation; see 117295)}$$$

Lean4

/-- Distance from the image of a point under inversion to the center. This formula accidentally
works for `x = c`. -/
theorem dist_inversion_center (c x : P) (R : ℝ) : dist (inversion c R x) c = R ^ 2 / dist x c :=
  by
  rcases eq_or_ne x c with (rfl | hx)
  · simp
  have : dist x c ≠ 0 := dist_ne_zero.2 hx
  simp only [inversion]
  field_simp
  simp only [sq, dist_vadd_left, norm_smul, norm_div, norm_mul, Real.norm_eq_abs, abs_mul_abs_self, abs_dist,
    ← dist_eq_norm_vsub]
  field_simp

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