inversion_inversion — Mathlib

English

Distance from the center to the inverted point equals R^2 divided by the distance from the center to the original point.

Русский

Расстояние от центра до инверсии равно R^2/dist(x,c).

LaTeX

$$$\operatorname{dist}(c, \operatorname{inversion}(c,R)x) = \dfrac{R^2}{\operatorname{dist}(x,c)}$$$

Lean4

@[simp]
theorem inversion_inversion (c : P) {R : ℝ} (hR : R ≠ 0) (x : P) : inversion c R (inversion c R x) = x :=
  by
  rcases eq_or_ne x c with (rfl | hne)
  · rw [inversion_self, inversion_self]
  · rw [inversion, dist_inversion_center, inversion_vsub_center, smul_smul, ← mul_pow, div_mul_div_comm,
      div_mul_cancel₀ _ (dist_ne_zero.2 hne), ← sq, div_self, one_pow, one_smul, vsub_vadd]
    exact pow_ne_zero _ hR

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