mathlib3
382acc15 - feat(geometry/manifold): generalize some lemmas from `smooth` to `cont_mdiff` (#15560)

Commit

3 years ago

feat(geometry/manifold): generalize some lemmas from `smooth` to `cont_mdiff` (#15560) Also add `*_within_at`, `*_at`, and `*_on` versions.

Author

urkud

Parents