Isometries of Euclidean space

TheoremIsometries of Euclidean space are affine#✓fully proved

For every natural number \(n\), every isometry \(f\) of the Euclidean space \(\mathbb{R}^n\) is affine: there is a linear map \(A : \mathbb{R}^n \to \mathbb{R}^n\), the linear part of \(f\), such that \(f(x) = A x + f(0)\) for every \(x \in \mathbb{R}^n\).

theorem isometry_apply_eq_linear_apply_add_map_zero {n : ℕ}
    (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hf : Isometry f) (x : EuclideanSpace ℝ (Fin n)) :
    f x = hf.affineIsometryOfStrictConvexSpace.toAffineMap.linear x + f 0

Used by 1

Used byIsometries of Euclidean space fixing the origin are linear

TheoremIsometries of Euclidean space fixing the origin are linear#✓fully proved

For every natural number \(n\), if \(f\) is an isometry of the Euclidean space \(\mathbb{R}^n\) with \(f(0) = 0\), then \(f\) is \(\mathbb{R}\)-linear: \(f(x + y) = f(x) + f(y)\) and \(f(c x) = c f(x)\) for all \(x, y \in \mathbb{R}^n\) and \(c \in \mathbb{R}\).

theorem isometry_isLinearMap_of_map_zero {n : ℕ}
    (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hf : Isometry f) (hf0 : f 0 = 0) :
    IsLinearMap ℝ f

Uses 1

Proof usesIsometries of Euclidean space are affine

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.