mathlib
545186ca - refactor(*): add a notation for `nhds_within` (#3683)

Commit

5 years ago

refactor(*): add a notation for `nhds_within` (#3683) The definition is still there and can be used too.

Author

urkud

Parents