mathlib

d0507e7b - feat(analysis/normed_space/affine_isometry): `subtypeₐᵢ` (#16573)

feat(analysis/normed_space/affine_isometry): `subtypeₐᵢ` (#16573) Now that we have `affine_subspace.subtype`, add the corresponding definition as a bundled affine isometry (so resolving a comment about that being missing). The name uses subscript `ₐᵢ` rather than superscript `ᵃⁱ` as in the notation for `affine_isometry` because Lean does not accept the superscript in identifiers.