inversion_injective

Mathlib.Geometry.Euclidean.Inversion.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanGeometry.inversion_injective

English

For nonzero radius, inversion is injective.

Русский

Для ненулевого радиуса инверсия инъективна.

LaTeX

$$$\text{Injective}(\operatorname{inversion}(c,R))$ if $R \neq 0$$$

Lean4

theorem inversion_injective (c : P) {R : ℝ} (hR : R ≠ 0) : Injective (inversion c R) :=
  (inversion_involutive c hR).injective

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

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

Разделы

Аффилиация

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