inversion — Mathlib

English

For any nonzero radius R, the inversion map with center c is an involution: applying it twice returns the original point.

Русский

При любом ненулевом радиусе R отображение инверсии с центром c является инволютивным: применение дважды возвращает исходную точку.

LaTeX

$$Inversion is an involution: (inversion c R) ∘ (inversion c R) = id$$

Lean4

/-- Inversion in a sphere in an affine space. This map sends each point `x` to the point `y` such
that `y -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ c)`, where `c` and `R` are the center and the radius the
sphere. -/
def inversion (c : P) (R : ℝ) (x : P) : P :=
  (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c

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