inversion_vsub_center

Mathlib.Geometry.Euclidean.Inversion.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanGeometry.inversion_vsub_center

English

The same relationship as in 117292; vector form of inversion displacement.

Русский

Та же зависимость в виде вектора относительно центра при инверсии.

LaTeX

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

Lean4

theorem inversion_vsub_center (c : P) (R : ℝ) (x : P) : inversion c R x -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ c) :=
  vadd_vsub _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru