mathlib3
06bb5b66 - feat(topology/nhds_set): define neighborhoods of a set (#11520)

Commit

4 years ago

feat(topology/nhds_set): define neighborhoods of a set (#11520) * Co-authored by @PatrickMassot * From the sphere eversion project

Author

fpvandoorn

Parents