compacts): add `positive_compacts.map` (#18872)

Commit

2 years ago

feat(topology/sets/compacts): add `positive_compacts.map` (#18872) Also adds some missing functorial lemmas about `map`.

Author

eric-wieser

Parents