Commit 2021-11-06 20:27 56a9228f
View on Github →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.