continuous_affine_map): isometry from space of continuous affine maps to product of codomain with space of continuous linear maps (#10201)

Commit

4 years ago

feat(analysis/normed_space/continuous_affine_map): isometry from space of continuous affine maps to product of codomain with space of continuous linear maps (#10201) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents

b9f7b4db

mathlib3 62621659 - feat(analysis/normed_space/continuous_affine_map): isometry from space of continuous affine maps to product of codomain with space of continuous linear maps (#10201)

mathlib3
62621659 - feat(analysis/normed_space/continuous_affine_map): isometry from space of continuous affine maps to product of codomain with space of continuous linear maps (#10201)