Commit 2022-12-24 02:09 09258fb7

feat(analysis/normed_space/affine_isometry, linear_algebra/affine_space/affine_equiv): restrict affine isometry to isometry equivalence (#17522) The main result in this commit is affine_subspace.isometry_equiv_map: Given an affine isometry, each of its affine subspaces is affine isometry equivalent to its image. isometry_equiv_map returns this isometry equivalence. The two other most significant results that are proved on the way are:

• affine_subspace.equiv_map_of_injective: Restricts an injective affine map to an affine equivalence of a subspace to its image (used by isometry_equiv_map)
• affine_equiv.of_bijective: obtain an affine equivalence from a bijective affine map The construction uses the new definition affine_equiv.of_bijective that makes an affine equivalence of a bijective affine map.