Def topological_space.open_nhds.inclusion

feat(topology/sheaves): the sheaf condition for functions satisfying a local predicate (#3906) …

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