Commit 2020-07-15 00:57 8495f76b

feat(geometry/manifold/times_cont_mdiff): smooth functions between manifolds (#3387) We define smooth functions between smooth manifolds, and prove their basic properties (including the facts that a composition of smooth functions is smooth, and that the tangent map of a smooth map is smooth). To avoid reproving always the same stuff in manifolds, we build a general theory of local invariant properties in the model space (i.e., properties which are local, and invariant under the structure groupoids) and show that the lift of such properties to charted spaces automatically inherit all the good behavior of the original property. We apply this general machinery to prove most basic properties of smooth functions between manifolds.