Isometries and crystallographic groups

Distance-preserving maps of Euclidean space, their classification, and discrete symmetry groups such as wallpaper and space groups.

TheoremBeckman–Quarles theorem#✓fully proved

Let \(n \ge 2\) and let \(f : \mathbb{R}^n \to \mathbb{R}^n\) be a map of \(n\)-dimensional real Euclidean space such that \(\lVert f(x) - f(y) \rVert = 1\) whenever \(\lVert x - y \rVert = 1\). Then \(f\) is an isometry, that is, \(\lVert f(x) - f(y) \rVert = \lVert x - y \rVert\) for all \(x, y \in \mathbb{R}^n\).

Surjectivity of \(f\) is neither assumed nor concluded.

theorem beckman_quarles
    {n : ℕ} (hn : 2 ≤ n)
    (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hf : ∀ x y : EuclideanSpace ℝ (Fin n), dist x y = 1 → dist (f x) (f y) = 1) :
    Isometry f
Sources
  • F. S. Beckman and D. A. Quarles Jr., On isometries of Euclidean spaces, Proc. Amer. Math. Soc. 4 (1953) 810–815 original theorem; standard formulation for ℝ^n, n ≥ 2.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.