compacts): add `positive_compacts.map`

Commit

2 years ago

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

References

Author

eric-wieser

Committer

eric-wieser

Parents