Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes