inversion_involutive — Mathlib

English

Inversion with nonzero radius is a surjective, involutive map; does not depend on orientation.

Русский

Инверсия с ненулевым радиусом является сюръективной инволюцией; не зависит от ориентации.

LaTeX

$$$\text{Inversion}(c,R) \text{ is an involution; in particular surjective for } R \neq 0$$$

Lean4

theorem inversion_involutive (c : P) {R : ℝ} (hR : R ≠ 0) : Involutive (inversion c R) :=
  inversion_inversion c hR

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