center_eq_inversion

Mathlib.Geometry.Euclidean.Inversion.Basic

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

English

For nonzero radius, the equation c = inversion(c, R, x) is equivalent to x = c.

Русский

При ненулевом радиусе уравнение c = inversion(c, R, x) эквивалентно x = c.

LaTeX

$$$R \ne 0 \Rightarrow (c = \operatorname{inversion}(c,R,x)) \iff x=c$$$

Lean4

theorem center_eq_inversion (hR : R ≠ 0) : c = inversion c R x ↔ x = c :=
  eq_comm.trans (inversion_eq_center hR)

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

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

Разделы

Аффилиация

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