inversion_of_mem_sphere

Mathlib.Geometry.Euclidean.Inversion.Basic

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

English

If x lies on the sphere of radius R centered at c, then inversion leaves x fixed.

Русский

Если x лежит на сфере радиуса R, центр которой в c, то inversion(c,R)x = x.

LaTeX

$$$x \in \mathrm{Sphere}(c,R) \Rightarrow \operatorname{inversion}(c,R)x = x$$$

Lean4

theorem inversion_of_mem_sphere (h : x ∈ Metric.sphere c R) : inversion c R x = x :=
  h.out ▸ inversion_dist_center c x

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

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

Разделы

Аффилиация

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