mathlib3
32c82274 - feat(analysis/normed_space/basic): define inclusion `locally_constant X G → C(X, G)` as various types of bundled morphism (#8448)

Commit
4 years ago
feat(analysis/normed_space/basic): define inclusion `locally_constant X G → C(X, G)` as various types of bundled morphism (#8448)
Author
Parents
Loading