inversion_eq_lineMap — Mathlib

English

The inversion map is given by a line map along the line from the center to x, with parameter depending on distance.

Русский

Инверсия описывается через отображение вдоль луча от центра к x, с параметром, зависящим от расстояния.

LaTeX

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

Lean4

theorem inversion_eq_lineMap (c : P) (R : ℝ) (x : P) : inversion c R x = lineMap c x ((R / dist x c) ^ 2) :=
  rfl

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