Affine map restrictions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines restrictions of affine maps.
Main definitions #
Main theorems #
- The associated linear map of the restriction is the restriction of the
linear map associated to the original affine map.
- The restriction is injective if the original map is injective.
- The restriction in surjective if the codomain is the image of the domain.
Restrict domain and codomain of an affine map to the given subspaces.