# Commit 2022-08-08 21:44 4ece2ee4

View on Github →feat(geometry/manifold/smooth_manifold_with_corners): properties to prove smoothness of mfderiv (#15523)

- Define
`achart`

- Rename and reformulate
`mem_maximal_atlas_of_mem_atlas -> subset_maximal_atlas`

- Used to prove smoothness of
`mfderiv`

(that result still has to be generalized to`mfderiv_within`

, so is not included yet) - From the sphere eversion project