mathlib3

361e2163 - feature(category_theory/instances/Top/open[_nhds]): category of open sets, and open neighbourhoods of a point (merge #920 first) (#922)

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