Commit 2019-04-16 07:19 361e2163

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