center_eq_inversion'

Mathlib.Geometry.Euclidean.Inversion.Basic

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

English

A centered simplification: c = inversion(c, R, x) is equivalent to x = c or R = 0.

Русский

Упрощение: c = inversion(c, R, x) эквивалентно x = c или R = 0.

LaTeX

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

Lean4

@[simp]
theorem center_eq_inversion' : c = inversion c R x ↔ x = c ∨ R = 0 :=
  eq_comm.trans inversion_eq_center'

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

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

Разделы

Аффилиация

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