Mathlib v3 is deprecated. Go to Mathlib v4

Def topological_space.open_nhds.open_nhds

Modification history

2019-10-03 17:37
src/topology/category/Top/open_nhds.lean
chore(*): fix errors in library and sanity_check (#1499) …
Deleted topological_space.open_nhds.open_nhdsView on Github →
2019-04-16 07:19
src/category_theory/instances/Top/open_nhds.lean
feature(category_theory/instances/Top/open[_nhds]): category of open sets, and open neighbourhoods of a point (merge #920 first) (#922) …
Added topological_space.open_nhds.open_nhdsView on Github →