inversion_mul — Mathlib

English

Distance from the center to the image under inversion scales as R^2 over the original distance.

Русский

Расстояние от центра до изображения после инверсии пропорционально R^2 делённому на исходное расстояние.

LaTeX

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

Lean4

theorem inversion_mul (c : P) (a R : ℝ) (x : P) : inversion c (a * R) x = homothety c (a ^ 2) (inversion c R x) := by
  simp only [inversion_eq_lineMap, ← homothety_eq_lineMap, ← homothety_mul_apply, mul_div_assoc, mul_pow]

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