mathlib3

f9f0ca6d - feat(analysic/calculus/times_cont_diff): add times_cont_diff_within_at (#3262)

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.