mathlib

56a9228f - feat(analysis/normed_space/continuous_affine_map): define bundled continuous affine maps (#10161)

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.