Commit 2021-11-06 20:27 56a9228f

feat(analysis/normed_space/continuous_affine_map): define bundled continuous affine maps (#10161) I want to use the result the evaluation map Hom(E, F) × E → F is smooth in a category with continuous affine maps as morphisms. It is convenient to have a bundled type for this, despite the necessary boilerplate (proposed here). Formalized as part of the Sphere Eversion project.