Mathlib v3 is deprecated. Go to Mathlib v4

Def is_open_map.adjunction_nhds

Modification history

2021-08-31 09:04
src/topology/category/Top/open_nhds.lean
feat(algebraic_geometry): Restriction of locally ringed spaces (#8809) …
Added is_open_map.adjunction_nhdsView on Github →