Def TopologicalSpace.OpenNhds

Modification history

2025-12-18 13:14
Mathlib/Topology/Category/TopCat/OpenNhds.lean
refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure (#26446) …
Modified TopologicalSpace.OpenNhdsView on Github →
2023-05-08 02:51
Mathlib/Topology/Category/Top/OpenNhds.lean
feat: port Topology.Category.Top.OpenNhds (#3834)
Added TopologicalSpace.OpenNhdsView on Github →