inversion_def — Mathlib

English

The inversion map is compatible with composition of homotheties: inversion with product radius corresponds to composing a homothety with the inverted image.

Русский

Инверсия совместима с композициями гомотетии: инверсия радиуса произведения эквивалентна композиции гомотетий над инвертированным изображением.

LaTeX

$$inversion c (a*R) x = homothety c (a^2) (inversion c R x)$$

Lean4

theorem inversion_def : inversion = fun (c : P) (R : ℝ) (x : P) => (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c :=
  rfl

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