# Commit 2019-04-16 07:19 361e2163

View on Github →feature(category_theory/instances/Top/open[_nhds]): category of open sets, and open neighbourhoods of a point (merge #920 first) (#922)

- rearrange Top
- oops, import from the future
- the categories of open sets and of open_nhds
- missing import
- restoring opens, adding headers
- Update src/category_theory/instances/Top/open_nhds.lean Co-Authored-By: semorrison scott@tqft.net
- use full_subcategory_inclusion