Mathlib v3 is deprecated. Go to Mathlib v4

Def topological_space.open_nhds

Modification history

2022-08-01 15:32
src/topology/category/Top/open_nhds.lean
refactor(category_theory): custom structure for full_subcategory (#14767) …
Modified topological_space.open_nhdsView on Github →
2020-08-28 03:16
src/topology/category/Top/open_nhds.lean
feat(topology/sheaves): the sheaf condition for functions satisfying a local predicate (#3906) …
Modified topological_space.open_nhdsView on Github →
2019-10-03 17:37
src/topology/category/Top/open_nhds.lean
chore(*): fix errors in library and sanity_check (#1499) …
Added topological_space.open_nhdsView on Github →