Mathlib v3 is deprecated. Go to Mathlib v4

Theorem topological_space.nhds_mk_of_nhds_single

Modification history

2022-09-19 07:18
src/topology/order.lean
refactor(topology/algebra/with_zero_topology): review API, golf (#16359) …
Added topological_space.nhds_mk_of_nhds_singleView on Github →