Commit 2026-07-22 17:22 9b53612f
View on Github →chore: golf proofs of mdifferentiableAt_atlas{_symm} (#42011)
- introduce
mdifferentiableAt_of_mem_maximalAtlasandmdifferentiableAt_symm_of_mem_maximalAtlas; these generalise the corresponding results to members of the maximal atlas; - golf the proofs of these lemmas by re-using the corresponding results about maximal atlas members being C^n.
The second bullet slightly strenthens an import dependency (of this file on the corresponding
C^nproofs): I consider this unproblematic since - that dependency was already implicit before,
- there does not seem a pressing need to tease apart imports further; if such need arises, this proof can be reverted,
- for #41796 (the first half of "the composition of immersions is an immersion"), I need versions of these lemmas for extended charts (which are known to be in the maximal atlas). This is a neat way to obtain this.