Commit 2020-07-15 00:57 8495f76b

View on Github →

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.

Estimated changes

added theorem times_cont_mdiff.comp
added theorem times_cont_mdiff.of_le
added def times_cont_mdiff
added theorem times_cont_mdiff_at_id
added theorem times_cont_mdiff_const
added theorem times_cont_mdiff_id
added theorem times_cont_mdiff_iff
added theorem times_cont_mdiff_on_id
added theorem times_cont_mdiff_top