opens): module-doc, cleanup, and construct some morphisms (#3601)

Commit

5 years ago

chore(topology/category/Top/opens): module-doc, cleanup, and construct some morphisms (#3601) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents

c63dad10

mathlib d952e8bf - chore(topology/category/Top/opens): module-doc, cleanup, and construct some morphisms (#3601)

mathlib
d952e8bf - chore(topology/category/Top/opens): module-doc, cleanup, and construct some morphisms (#3601)