Commit 2024-11-08 15:36 dbba5180

feat: version within a set of ContMDiffAt.mfderiv (#18724) Solving a todo, we give a version within a set of the result ContMDiffAt.mfderiv saying that mfderiv (f x) (g x) is smooth when f is a smooth family of maps, and g is a smooth basepoint. For this, we streamline the proof of ContMDiffAt.mfderiv, avoiding all defeq abuses, and then we complexify it by adding suitable neighborhoods where needed. A very positive outcome of the localized lemma is that it implies readily that the tangent map to a smooth map is smooth (as a map between tangent bundles), making it possible to replace a messy 250 lines arguments by a conceptual 25 lines argument (so that the PR has overall a net line decrease of 50 lines). This relies on a new general lemma ContMDiffWithinAt.clm_apply_of_inCoordinates saying that, if a map of vector bundles is smooth in coordinates, then applying it to a smooth section gives a smooth map -- a result which is obvious in retrospect, but where finding the right statement is not so obvious.