Isometries and crystallographic groups
Distance-preserving maps of Euclidean space, their classification, and discrete symmetry groups such as wallpaper and space groups.
- Classification of plane isometries
- Crystallographic groups
- Discrete groups of plane isometries
- Isometries of Euclidean space
TheoremBeckman–Quarles theorem#✓fully proved
MathlibExt.Geometry.Euclidean.BeckmanQuarlesWanted.beckman_quarles
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
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.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.