inversion_self — Mathlib

English

Inversion with center c and radius R (R ≠ 0) is an involution: applying it twice yields identity.

Русский

Инверсия с центром c и радиусом R (R ≠ 0) является инволюцией: повторное применение даёт тождественное отображение.

LaTeX

$$$\text{If } R \neq 0:\quad (\operatorname{inversion}(c,R))^2 = \mathrm{id}$$$

Lean4

@[simp]
theorem inversion_self (c : P) (R : ℝ) : inversion c R c = c := by simp [inversion]

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