inversion_bijective — Mathlib

English

Let c be a fixed center in the Euclidean space and R ≠ 0 a fixed radius. The inversion map x ↦ inversion(c, R, x) is a bijection of the space onto itself; in particular, it has a two-sided inverse and is one-to-one and onto.

Русский

Пусть c — фиксированная точка центра в евклидовом пространстве и R ≠ 0 — фиксированный радиус. Отображение инверсии x ↦ inversion(c, R, x) является биекцией пространства в себя: оно взаимно однозначно и сюръективно.

LaTeX

$$$R e 0 \quad\Longrightarrow\quad \operatorname{Bijective}\big(\operatorname{inversion}(c,R)\big)$$$

Lean4

theorem inversion_bijective (c : P) {R : ℝ} (hR : R ≠ 0) : Bijective (inversion c R) :=
  (inversion_involutive c hR).bijective

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