inversion_eq_center'

Mathlib.Geometry.Euclidean.Inversion.Basic

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

English

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

Русский

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

LaTeX

$$$(R \ne 0) \Rightarrow\; inversion(c,R,x)=c \iff x=c \lor R=0$$$

Lean4

@[simp]
theorem inversion_eq_center' : inversion c R x = c ↔ x = c ∨ R = 0 := by
  by_cases hR : R = 0 <;> simp [inversion_eq_center, hR]

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

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

Разделы

Аффилиация

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