inversion_eq_center — Mathlib

English

If R ≠ 0, then the only solution to inversion(c, R, x) = c is x = c; i.e., the center c is a fixed point only for x = c.

Русский

Если R ≠ 0, то единственным решением уравнения inversion(c, R, x) = c является x = c; т. е. центр c является фиксированной точкой только для x = c.

LaTeX

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

Lean4

theorem inversion_eq_center (hR : R ≠ 0) : inversion c R x = c ↔ x = c :=
  (inversion_injective c hR).eq_iff' <| inversion_self _ _

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