Theorem mdifferentiableAt_of_mem_maximalAtlas

Modification history

2026-07-22 17:22
Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
chore: golf proofs of `mdifferentiableAt_atlas{_symm}` (#42011) …
Added mdifferentiableAt_of_mem_maximalAtlasView on Github →