mathlib
e21dc7a9 - feat(topology/subset_properties): define `filter.cocompact` (#4666)

Commit

5 years ago

feat(topology/subset_properties): define `filter.cocompact` (#4666) The filter of complements to compact subsets.

References

Author

urkud

Parents