Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-07 13:00 e354e865

View on Github →

feat(geometry/manifold): lemmas from the sphere eversion project (#18877)

  • Also adds a new library note comp_of_eq lemmas about how (I think) we should better formulate composition lemmas of properties of functions.
  • About the library note comp_of_eq lemmas: exactly the same problems happen in Lean 4.
  • renamings
smooth_iff_proj_smooth -> smooth_prod_iff
differentiable_at.fderiv_within_prod -> differentiable_within_at.fderiv_within_prod
  • We add a path_connected_space instance of the tangent space. This instance is sufficient to compile sphere-eversion, without any normed_space instances on the tangent space (which are not the canonical structure on the tangent space).
  • From the sphere eversion project

Estimated changes