mathlib
ca93096b - feat(topology/nhds_set): add `has_basis_nhds_set` (#12908)

Commit

3 years ago

feat(topology/nhds_set): add `has_basis_nhds_set` (#12908) Also add `nhds_set_union`.

Author

urkud

Parents