Commit 2020-07-03 15:04 f9f0ca6d

feat(analysic/calculus/times_cont_diff): add times_cont_diff_within_at (#3262) I want to refactor manifolds, defining local properties in the model space and showing that they automatically inherit nice behavior in manifolds. In this PR, we modify a little bit the definition of smooth functions in vector spaces by introducing a predicate times_cont_diff_within_at (just like we already have continuous_within_at or differentiable_within_at) and using it in all definitions and proofs. This will be the basis of the locality argument in manifolds.