mathlib3

09110f10 - feat(geometry/manifold/bump_function): define smooth bump functions, baby version of the Whitney embedding thm (#6839)

feat(geometry/manifold/bump_function): define smooth bump functions, baby version of the Whitney embedding thm (#6839) * refactor some functions in `analysis/calculus/specific_functions` to use bundled structures; * define `to_euclidean`, `euclidean.dist`, `euclidean.ball`, and `euclidean.closed_ball`; * define smooth bump functions on manifolds; * prove a baby version of the Whitney embedding theorem.