mathlib3
1e0761e5 - feat(topology/maps): closed embeddings (#1013)

Commit

6 years ago

feat(topology/maps): closed embeddings (#1013) * feat(topology/maps): closed embeddings * fix "is_open_map"

References

Author

rwbarton

Committer

mergify[bot]

Parents