inversion_surjective — Mathlib

English

For nonzero radius, inversion is onto; every point is attained as an image of some point.

Русский

Для ненулевого радиуса инверсия охватывает всю пространство; любая точка является образом некоторой точки.

LaTeX

$$$\text{Surjective}(\operatorname{inversion}(c,R))$ for $R \neq 0$$$

Lean4

theorem inversion_surjective (c : P) {R : ℝ} (hR : R ≠ 0) : Surjective (inversion c R) :=
  (inversion_involutive c hR).surjective

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